diff --git a/src/Std/Internal.lean b/src/Std/Internal.lean index 4aac6fd85ce7..cea98df740a5 100644 --- a/src/Std/Internal.lean +++ b/src/Std/Internal.lean @@ -9,6 +9,7 @@ prelude public import Std.Internal.Async public import Std.Internal.Parsec public import Std.Internal.UV +public import Std.Internal.Http @[expose] public section diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index fa6285edd138..49830c407691 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -138,6 +138,13 @@ Construct an `ETask` that is already resolved with value `x`. protected def pure (x : α) : ETask ε α := Task.pure <| .ok x +/-- +Returns `true` if a `ETask` has finished it's execution +-/ +@[inline] +protected def isFinished (x : ETask ε α) : BaseIO Bool := do + return (← IO.getTaskState x) == IO.TaskState.finished + /-- Creates a new `ETask` that will run after `x` has finished. If `x`: - errors, return an `ETask` that resolves to the error. @@ -242,6 +249,13 @@ Construct an `AsyncTask` that is already resolved with value `x`. protected def pure (x : α) : AsyncTask α := Task.pure <| .ok x +/-- +Returns `true` if a `AsyncTask` has finished it's execution +-/ +@[inline] +protected def isFinished (x : AsyncTask α) : BaseIO Bool := do + return (← IO.getTaskState x) == IO.TaskState.finished + /-- Create a new `AsyncTask` that will run after `x` has finished. If `x`: diff --git a/src/Std/Internal/Http.lean b/src/Std/Internal/Http.lean new file mode 100644 index 000000000000..6779299342b2 --- /dev/null +++ b/src/Std/Internal/Http.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Data +public import Std.Internal.Http.Server + +public section + +namespace Std +namespace Http + +set_option linter.all true + +/-! +# Http + +A "low-level" HTTP 1.1 implementation for Lean. It is designed to be used with or without the +`Async` library if you want to implement a custom `Connection`. + +# Overview + +This module of the standard library defines many concepts related to the HTTP protocol +and its semantics in a Sans-IO format. The main function of this library is `Std.Http.Server.serve`, +located in the module `Std.Internal.Http.Server`. It starts a simple HTTP/1.1 server that +handles all requests and sends them to a simple handler function. It uses the default `Std.Internal.Async` +library, but it can be customized to use whatever IO library you want, as the protocol implementation +is pure. + +If you want to customize how your server handles sockets, you can use `Std.Http.Server.serveConnection`, +which is a simple function to bind a handler to a `ClientConnection`. + +# Low-Level Protocol Implementation + +This library provides a low-level foundation that allows you to implement your own IO layer on top +of it. The core protocol parsing and generation logic is available in `Std.Internal.Http.Protocol`, +which provides pure functions for HTTP message parsing and serialization. This design allows you to +integrate the HTTP protocol handling with any IO system or networking library of your choice, while +reusing the robust protocol implementation. + +# Minimal Example + +```lean +import Std.Internal.Http +import Std.Internal.Async + +open Std.Internal.IO.Async +open Std Http + +def handler (req : Request Body) : Async (Response Body) := do + let some data ← req.body.collectString + | return Response.badRequest "expected a utf8 body" + + return Response.ok ("hi, " ++ data) + +def mainAsync : Async Unit := do + Server.serve (.v4 (.mk (.ofParts 0 0 0 0) 8080)) handler + +def main := mainAsync.block +``` +-/ diff --git a/src/Std/Internal/Http/Data.lean b/src/Std/Internal/Http/Data.lean new file mode 100644 index 000000000000..266c26be53d6 --- /dev/null +++ b/src/Std/Internal/Http/Data.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Data.Body +public import Std.Internal.Http.Data.Headers +public import Std.Internal.Http.Data.Method +public import Std.Internal.Http.Data.Version +public import Std.Internal.Http.Data.Request +public import Std.Internal.Http.Data.Response +public import Std.Internal.Http.Data.URI +public import Std.Internal.Http.Data.Status +public import Std.Internal.Http.Data.Version diff --git a/src/Std/Internal/Http/Data/Body.lean b/src/Std/Internal/Http/Data/Body.lean new file mode 100644 index 000000000000..fbbbc0e9c519 --- /dev/null +++ b/src/Std/Internal/Http/Data/Body.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Data.Body.Length +public import Std.Internal.Http.Data.Body.ByteStream + +public section + +open Std Internal IO Async + +namespace Std +namespace Http + +set_option linter.all true + +/-- +Type that represents the body of a request or response with streams of bytearrays or bytearrays of fixed +size. +-/ +inductive Body where + /-- + Empty body with no content + -/ + | zero + + /-- + Body containing raw byte data stored in memory + -/ + | bytes (data : ByteArray) + + /-- + Body containing streaming data from a byte stream channel + -/ + | stream (channel : Body.ByteStream) +deriving Inhabited + +namespace Body + +/-- +Get content length of a body (if known). +-/ +def getContentLength (body : Body) : Length := + match body with + | zero => .fixed 0 + | .bytes data => .fixed data.size + | .stream _ => .chunked + +/-- +Close the body and release any associated resources. For streaming bodies, this closes the underlying channel. +For other body types, this is a no-op. +-/ +def close (body : Body) : Async Unit := + match body with + | .stream channel => channel.close + | _ => pure () + +instance : Coe String Body where + coe := .bytes ∘ String.toUTF8 + +instance : Coe ByteArray Body where + coe := .bytes + +instance : Coe Body.ByteStream Body where + coe := .stream + +/-- +Iterate over the body content in chunks, processing each ByteArray chunk with the given step function. +This allows for memory-efficient processing of large bodies without loading everything into memory at once. +-/ +@[inline] +protected partial def forIn + {β : Type} (body : Body) (acc : β) + (step : ByteArray → β → Async (ForInStep β)) : + Async β := do + let rec @[specialize] loop (stream : ByteStream) (acc : β) : Async β := do + if let some data ← stream.recv then + match ← step data acc with + | .done res => pure res + | .yield res => loop stream res + else + return acc + + match body with + | .zero => pure acc + | .bytes data => + match ← step data acc with + | .done x => pure x + | .yield x => pure x + | .stream strea => loop strea acc + +instance : ForIn Async Body ByteArray where + forIn := Body.forIn + +/-- +Collect all data from the body into a single `ByteArray`. This reads the entire body content into memory, +so use with caution for large bodies as it may consume significant memory. +-/ +def collectByteArray (body : Body) : Async ByteArray := do + let mut result := .empty + for x in body do result := result ++ x + return result + +/-- +Collect all data from the body into a single `String`. This reads the entire body content into memory, +so use with caution for large bodies as it may consume significant memory. If it's a valid UTF8 string +then it will return `some` otherwise `none`. +-/ +def collectString (body : Body) : Async (Option String) := do + let mut result := .empty + for x in body do result := result ++ x + return String.fromUTF8? result diff --git a/src/Std/Internal/Http/Data/Body/ByteStream.lean b/src/Std/Internal/Http/Data/Body/ByteStream.lean new file mode 100644 index 000000000000..16da23d0cf85 --- /dev/null +++ b/src/Std/Internal/Http/Data/Body/ByteStream.lean @@ -0,0 +1,285 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Sync +public import Std.Internal.Async +public import Std.Internal.Async.IO +public import Std.Internal.Http.Util.BufferBuilder + +public section + +open Std Internal IO Async + +namespace Std +namespace Http +namespace Body + +set_option linter.all true + +/-! +This module defines the `ByteStream` structure that is a channel for byte arrays. +-/ + +public section + +private structure ByteStream.Consumer (α : Type) where + promise : IO.Promise Bool + waiter : Option (Internal.IO.Async.Waiter (Option α)) + +private def ByteStream.Consumer.resolve (c : ByteStream.Consumer α) (b : Bool) : BaseIO Unit := + c.promise.resolve b + +private structure ByteStream.State where + buffer : Util.BufferBuilder := .empty + knownSize : Option Nat := none + closed : Bool := false + waiting : Queue (ByteStream.Consumer ByteArray) := .empty + backpressureWaiting : Queue (IO.Promise Unit) := .empty + maxBufferSize : Nat := 8 * 1024 * 1024 + +/-- +A channel for byte arrays. +-/ +structure ByteStream where + private mk :: + private state : Std.Mutex ByteStream.State + +namespace ByteStream + +/-- +Creates a new ByteStream with a specified initial capacity. +-/ +def emptyWithCapacity (maxBufferSize : Nat := 8 * 1024 * 1024) : Async ByteStream := do + let state ← Std.Mutex.new { maxBufferSize := maxBufferSize } + return { state } + +/-- +Creates a new ByteStream with default capacity. +-/ +def empty : Async ByteStream := + emptyWithCapacity + +private def tryRecvFromBuffer' + [MonadState State (AtomicT State m)] [MonadLiftT BaseIO m] [Monad m] : + AtomicT State m (Option Util.BufferBuilder) := do + let state ← get + + if state.buffer.isEmpty then + if state.closed then + return none + else + return some .empty + else + modify fun s => { s with buffer := .empty } + + if let some (promise, rest) := state.backpressureWaiting.dequeue? then + discard <| promise.resolve () + modify fun s => { s with backpressureWaiting := rest } + + return some state.buffer + + private def tryRecv' (stream : ByteStream) : Async (Option Util.BufferBuilder) := do + stream.state.atomically tryRecvFromBuffer' + +/-- +Tries to receive all the current available data, it returns `some` when the channel is not closed +and contains some data. +-/ +def tryRecv (stream : ByteStream) : Async (Option ByteArray) := do + stream.state.atomically do + let buf ← tryRecvFromBuffer' + return Util.BufferBuilder.toByteArray <$> buf + +/-- +Receives (reads) all currently available data from the stream, emptying it. +Returns `none` if the stream is closed and no data is available. +-/ +partial def recv (stream : ByteStream) : Async (Option ByteArray) := do + let result ← stream.state.atomically do + if let some bb ← tryRecvFromBuffer' then + if bb.isEmpty then + let state ← get + if state.closed then + return Sum.inr none + else + let newPromise ← IO.Promise.new + modify fun s => { s with waiting := s.waiting.enqueue ⟨newPromise, none⟩ } + return Sum.inl newPromise + else + return Sum.inr (some bb) + else + return Sum.inr none + + match result with + | .inr res => return Util.BufferBuilder.toByteArray <$> res + | .inl promise => + try + discard <| await promise + recv stream + catch + _ => return none + +/-- +Sends (writes) data to the stream, appending it to existing contents. +Returns `false` if the stream is closed or data is empty. +-/ +partial def send (stream : ByteStream) (data : ByteArray) : Async Bool := do + if data.isEmpty then + return true + + let result ← stream.state.atomically do + let state ← get + + if state.closed then + return Sum.inr false + + let newSize := state.buffer.size + data.size + + if newSize >= state.maxBufferSize then + let promise ← IO.Promise.new + modify fun s => { s with backpressureWaiting := s.backpressureWaiting.enqueue promise } + return Sum.inl promise + else + modify fun s => { s with buffer := s.buffer.append data } + + if let some (consumer, rest) := state.waiting.dequeue? then + discard <| consumer.resolve true + modify fun s => { s with waiting := rest } + + return Sum.inr true + + match result with + | .inr r => return r + | .inl backpressurePromise => + try + await backpressurePromise + send stream data + catch + _ => return false + +/-- +Gets the known size of the stream if available. +Returns `none` if the size is not known. +-/ +def getKnownSize (stream : ByteStream) : Async (Option Nat) := do + stream.state.atomically do + let state ← get + return state.knownSize + +/-- +Sets the known size of the stream. +This is typically used when the total expected size is known ahead of time. +-/ +def setKnownSize (stream : ByteStream) (size : Option Nat) : Async Unit := do + stream.state.atomically do + modify fun s => { s with knownSize := size } + +/-- +Closes the stream, preventing further writes and causing pending/future +recv operations to return `none` when no data is available. +-/ +def close (stream : ByteStream) : Async Unit := do + stream.state.atomically do + let state ← get + if ¬ state.closed then + modify fun s => { s with closed := true } + + for consumer in state.waiting.toArray do + discard <| consumer.resolve false + + modify fun s => { s with waiting := .empty } + + for promise in state.backpressureWaiting.toArray do + discard <| promise.resolve () + + modify fun s => { s with backpressureWaiting := .empty } + +/-- +Checks if the stream is closed. +-/ +def isClosed (stream : ByteStream) : Async Bool := do + stream.state.atomically do + let state ← get + return state.closed + +/-- +Checks if the stream is empty. +-/ +def isEmpty (stream : ByteStream) : Async Bool := do + stream.state.atomically do + let state ← get + return state.buffer.isEmpty + +/-- +Returns `true` if data is ready to be received without blocking. +-/ +private def recvReady' : AtomicT State IO Bool := do + let state ← get + return ¬ state.buffer.isEmpty ∨ state.closed + +/-- +Creates a `Selector` that resolves once the `ByteStream` has data available and provides that data. +-/ +partial def recvSelector (stream : ByteStream) : Selector (Option ByteArray) where + tryFn := do + stream.state.atomically do + let state ← get + if ¬ state.buffer.isEmpty ∨ state.closed then + let val ← tryRecvFromBuffer' + return some (Util.BufferBuilder.toByteArray <$> val) + else + return none + + registerFn waiter := registerAux stream waiter + + unregisterFn := do + stream.state.atomically do + let state ← get + let waiters ← state.waiting.filterM fun c => do + match c.waiter with + | some waiter => return !(← waiter.checkFinished) + | none => return true + + modify fun s => { s with waiting := waiters } +where + registerAux (stream : ByteStream) (waiter : Waiter (Option ByteArray)) : IO Unit := do + stream.state.atomically do + if ← recvReady' then + let lose := do + let state ← get + if let some (consumer, waiters) := state.waiting.dequeue? then + discard <| consumer.resolve true + modify fun s => { s with waiting := waiters } + + let win promise := do + let val ← tryRecvFromBuffer' + promise.resolve (.ok (Util.BufferBuilder.toByteArray <$> val)) + + waiter.race lose win + else + let promise ← IO.Promise.new + modify fun s => { s with waiting := s.waiting.enqueue ⟨promise, some waiter⟩ } + + IO.chainTask promise.result? fun res? => do + match res? with + | none => return () + | some res => + if res then + registerAux stream waiter + else + let lose := return () + let win promise := promise.resolve (.ok none) + waiter.race lose win + +instance : IO.AsyncRead ByteStream (Option ByteArray) where + read stream := stream.recv + +instance : IO.AsyncWrite ByteStream ByteArray where + write stream data := do discard <| stream.send data + +end ByteStream diff --git a/src/Std/Internal/Http/Data/Body/Length.lean b/src/Std/Internal/Http/Data/Body/Length.lean new file mode 100644 index 000000000000..2e5b8bc80216 --- /dev/null +++ b/src/Std/Internal/Http/Data/Body/Length.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.Repr + +public section + +namespace Std +namespace Http +namespace Body + +set_option linter.all true + +/-- +Size of the body of a response or request. +-/ +inductive Length + /-- + Indicates that the HTTP message body uses **chunked transfer encoding**. + -/ + | chunked + + /-- + Indicates that the HTTP message body has a **fixed, known length**, as specified + by the `Content-Length` header. + -/ + | fixed (n : Nat) +deriving Repr, BEq + +namespace Length + +/-- +Checks if the `Length` is chunked. +-/ +def isChunked : Length → Bool + | .chunked => true + | _ => false + +end Length diff --git a/src/Std/Internal/Http/Data/Headers.lean b/src/Std/Internal/Http/Data/Headers.lean new file mode 100644 index 000000000000..fdbabc0ee8f3 --- /dev/null +++ b/src/Std/Internal/Http/Data/Headers.lean @@ -0,0 +1,266 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.Slice +public import Std.Data.HashMap +public import Std.Data.HashMap +public import Std.Data.HashSet +public import Std.Internal.Http.Encode + +public section + +namespace Std +namespace Http + +set_option linter.all true + +open Std + +/-- +Checks if a character is valid for use in an HTTP header value. +Valid characters include: +- Characters with values > 0x7F (extended ASCII) +- Tab character (0x09) +- Space character (0x20) +- Printable ASCII characters (0x21 to 0x7E) +-/ +@[expose] +def isValidHeaderCharNode (c : Char) : Bool := + (0x21 ≤ c.val ∧ c.val ≤ 0x7E) ∨ c.val = 0x09 ∨ c.val = 0x20 + +/-- +Proposition that asserts all characters in a string are valid for HTTP header values. +-/ +@[expose] +abbrev isValidHeaderValue (s : String) : Prop := + s.data.all isValidHeaderCharNode + +/-- +A validated HTTP header value that ensures all characters conform to HTTP standards. +-/ +structure HeaderValue where + /-- + The string data + -/ + value : String + + /-- + The proof that it's a valid header value + -/ + validHeaderValue : isValidHeaderValue value +deriving BEq, Repr + +namespace HeaderValue + +instance : Hashable HeaderValue where + hash x := Hashable.hash x.value + +instance : Inhabited HeaderValue where default := ⟨"", by decide⟩ + +/-- +Creates a new `HeaderValue` from a string with an optional proof of validity. +If no proof is provided, it attempts to prove validity automatically. +-/ +@[expose] +def new (s : String) (h : s.data.all isValidHeaderCharNode := by decide) : HeaderValue := + ⟨s, h⟩ + +/-- +Attempts to create a `HeaderValue` from a `String`, returning `none` if the string +contains invalid characters for HTTP header values. +-/ +@[expose] +def ofString? (s : String) : Option HeaderValue := + if h : s.data.all isValidHeaderCharNode then + some ⟨s, h⟩ + else + none + +/-- +Creates a `HeaderValue` from a string, panicking with an error message if the +string contains invalid characters for HTTP header values. +-/ +@[expose] +def ofString! (s : String) : HeaderValue := + if h : s.data.all isValidHeaderCharNode then + ⟨s, h⟩ + else + panic! s!"invalid header value: {s.quote}" + +/-- +Performs a case-insensitive comparison between a `HeaderValue` and a `String`. +Returns `true` if they match. +-/ +@[expose] +def is (s : HeaderValue) (h : String) : Bool := + s.value.toLower == h.toLower + +/-- +Concatenates two `HeaderValue` instances, preserving the validity guarantee. +-/ +def append (l : HeaderValue) (r : HeaderValue) : HeaderValue := by + refine ⟨l.value ++ r.value, ?_⟩ + unfold isValidHeaderValue + rw [String.data_append] + rw [List.all_append] + rw [Bool.and_eq_true] + constructor + · exact l.validHeaderValue + · exact r.validHeaderValue + +instance : HAppend HeaderValue HeaderValue HeaderValue where + hAppend := HeaderValue.append + +/-- +Joins an array of `HeaderValue` instances with comma-space separation. +Returns a single `HeaderValue` containing all values joined together. +If the array is empty, returns an empty `HeaderValue`. +-/ +def joinCommaSep (x : Array HeaderValue) : HeaderValue := + if h : 0 < x.size then + let first := x[0]'h + let rest := x[1...*] + rest.foldl (· ++ HeaderValue.new ", " ++ ·) first + else + .new "" + +end HeaderValue + +/-- +A structure for managing HTTP headers as key-value pairs. +-/ +structure Headers where + /-- + The internal hashmap that stores all the data. + -/ + data : HashMap String (String × (Array HeaderValue)) + +deriving Repr, Inhabited + +namespace Headers + +/-- +Tries to retrieve the `HeaderValue` for the given key. +Returns `none` if the header is absent. +-/ +@[inline] +def get? (headers : Headers) (name : String) : Option HeaderValue := + headers.data.get? name.toLower + |>.map (.joinCommaSep ∘ Prod.snd) + +/-- +Tries to check if the entry is present in the `Headers` +-/ +@[inline] +def hasEntry (headers : Headers) (name : String) (value : String) : Bool := + headers.data.get? name.toLower + |>.map Prod.snd + |>.bind (·.find? (·.is value)) + |>.isSome + +/-- +Tries to retrieve the last header value for the given key. +Returns `none` if the header is absent. +-/ +@[inline] +def getLast? (headers : Headers) (name : String) : Option HeaderValue := + headers.data.get? name.toLower + |>.bind (fun x => let arr := Prod.snd x; arr[arr.size - 1]?) + + +/-- +Like `get?`, but returns an empty HashSet if absent. +-/ +@[inline] +def getD (headers : Headers) (name : String) (d : HeaderValue) : HeaderValue := + headers.get? name |>.getD d + +/-- +Like `get?`, but panics if absent. +-/ +@[inline] +def get! (headers : Headers) (name : String) : HeaderValue := + headers.get? name |>.get! + +/-- +Inserts a new key-value pair into the headers. +-/ +@[inline] +def insert (headers : Headers) (name : String) (value : HeaderValue) : Headers := + let key := name.toLower + + if let some (_, headerValue) := headers.data.get? key then + { data := headers.data.insert key (name, headerValue.push value) } + else + { data := headers.data.insert key (name, #[value]) } + +/-- +Inserts a new key with an array of values. +-/ +@[inline] +def insertMany (headers : Headers) (name : String) (value : Array HeaderValue) : Headers := + let key := name.toLower + + if let some (_, headerValue) := headers.data.get? key then + { data := headers.data.insert key (name, headerValue ++ value) } + else + { data := headers.data.insert key (name, value) } + +/-- +Creates empty headers. +-/ +def empty : Headers := + { data := ∅ } + +/-- +Creates headers from a list of key-value pairs. +-/ +def ofList (pairs : List (String × HeaderValue)) : Headers := + { data := HashMap.ofList (pairs.map (fun (k, v) => (k.toLower, (k, #[v])))) } + +/-- +Checks if a header with the given name exists. +-/ +@[inline] +def contains (headers : Headers) (name : String) : Bool := + headers.data.contains name.toLower + +/-- +Removes a header with the given name. +-/ +@[inline] +def erase (headers : Headers) (name : String) : Headers := + { data := headers.data.erase name.toLower } + +/-- +Gets the number of headers. +-/ +@[inline] +def size (headers : Headers) : Nat := + headers.data.size + +/-- +Checks if the headers are empty. +-/ +@[inline] +def isEmpty (headers : Headers) : Bool := + headers.data.isEmpty + +/-- +Merges two headers, with the second taking precedence for duplicate keys. +-/ +def merge (headers1 headers2 : Headers) : Headers := + headers2.data.fold (fun acc k (_, v) => acc.insertMany k v) headers1 + +instance : ToString Headers where + toString headers := + let pairs := headers.data.toList.map (fun (_, (k, vs)) => s!"{k}: {HeaderValue.joinCommaSep vs |>.value}") + String.intercalate "\r\n" pairs + +instance : Encode .v11 Headers where + encode buffer := buffer.writeString ∘ toString diff --git a/src/Std/Internal/Http/Data/Method.lean b/src/Std/Internal/Http/Data/Method.lean new file mode 100644 index 000000000000..ffda838d547a --- /dev/null +++ b/src/Std/Internal/Http/Data/Method.lean @@ -0,0 +1,105 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.Repr +public import Std.Internal.Http.Encode + +public section + +namespace Std +namespace Http + +set_option linter.all true + +/-- +A method is a verb that describes the action to be performed. + +* Reference: https://httpwg.org/specs/rfc9110.html#methods +-/ +inductive Method where + /-- + Retrieve a resource. + -/ + | get + + /-- + Retrieve headers for a resource, without the body. + -/ + | head + + /-- + Submit data to be processed (e.g., form submission). + -/ + | post + + /-- + Replace a resource with new data. + -/ + | put + + /-- + Remove a resource. + -/ + | delete + + /-- + Establish a tunnel to a server (often for TLS). + -/ + | connect + + /-- + Describe communication options for a resource. + -/ + | options + + /-- + Perform a message loop-back test. + -/ + | trace + + /-- + Apply partial modifications to a resource. + -/ + | patch +deriving Repr, Inhabited, BEq + +namespace Method + +/-- +Converts a `String` into a `Method`. +-/ +def fromString? : String → Option Method + | "GET" => some .get + | "HEAD" => some .head + | "POST" => some .post + | "PUT" => some .put + | "DELETE" => some .delete + | "CONNECT" => some .connect + | "OPTIONS" => some .options + | "TRACE" => some .trace + | "PATCH" => some .patch + | _ => none + +instance : ToString Method where + toString + | .get => "GET" + | .head => "HEAD" + | .post => "POST" + | .put => "PUT" + | .delete => "DELETE" + | .connect => "CONNECT" + | .options => "OPTIONS" + | .trace => "TRACE" + | .patch => "PATCH" + +instance : Encode .v11 Method where + encode buffer := buffer.writeString ∘ toString + +end Method +end Http +end Std diff --git a/src/Std/Internal/Http/Data/Request.lean b/src/Std/Internal/Http/Data/Request.lean new file mode 100644 index 000000000000..748a2650d9dc --- /dev/null +++ b/src/Std/Internal/Http/Data/Request.lean @@ -0,0 +1,209 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Encode +public import Std.Internal.Http.Data.Body +public import Std.Internal.Http.Data.Headers +public import Std.Internal.Http.Data.Method +public import Std.Internal.Http.Data.Version +public import Std.Internal.Http.Data.URI + +public section + +namespace Std +namespace Http + +set_option linter.all true + +open Lean + +/-- +The main parts of a request containing the HTTP method, version, URI, and headers. +-/ +structure Request.Head where + /-- + The HTTP method (GET, POST, PUT, DELETE, etc.) for the request + -/ + method : Method := .get + + /-- + The HTTP protocol version (HTTP/1.0, HTTP/1.1, HTTP/2.0, etc.) + -/ + version : Version := .v11 + + /-- + The request target/URI indicating the resource being requested + -/ + uri : RequestTarget := .asteriskForm + + /-- + Collection of HTTP headers for the request (Content-Type, Authorization, etc.) + -/ + headers : Headers := .empty +deriving Inhabited, Repr + +/-- +HTTP request structure parameterized by body type +-/ +structure Request (t : Type) where + /-- + The request headers and metadata + -/ + head : Request.Head + + /-- + The request body content of type t + -/ + body : t +deriving Inhabited + +/-- +Builds a HTTP Request +-/ +structure Request.Builder where + /-- + The head of the request + -/ + head : Head := {} + +namespace Request + +instance : ToString Head where + toString req := + toString req.method ++ " " ++ + toString req.uri ++ " " ++ + toString req.version ++ + "\r\n" ++ + toString req.headers ++ "\r\n\r\n" + +/-- +Creates a new HTTP Request builder with default head (method: GET, version: HTTP/1.1, asterisk URI, empty headers) +-/ +def new : Builder := { } + +namespace Builder + +/-- +Creates a new HTTP Request builder with default head (method: GET, version: HTTP/1.1, asterisk URI, empty headers) +-/ +def empty : Builder := { } + +/-- +Sets the HTTP method for the request being built +-/ +def method (builder : Builder) (method : Method) : Builder := + { builder with head := { builder.head with method := method } } + +/-- +Sets the HTTP version for the request being built +-/ +def version (builder : Builder) (version : Version) : Builder := + { builder with head := { builder.head with version := version } } + +/-- +Sets the request target/URI for the request being built +-/ +def uri (builder : Builder) (uri : RequestTarget) : Builder := + { builder with head := { builder.head with uri := uri } } + +/-- +Sets the request target/URI for the request being built +-/ +def uri! (builder : Builder) (uri : String) : Builder := + { builder with head := { builder.head with uri := RequestTarget.parse! uri } } + +/-- +Adds a single header to the request being built +-/ +def header (builder : Builder) (key : String) (value : HeaderValue) : Builder := + { builder with head := { builder.head with headers := builder.head.headers.insert key value } } + +/-- +Builds and returns the final HTTP Request with the specified body +-/ +def body (builder : Builder) (body : t) : Request t := + { head := builder.head, body := body } + +/-- +Builds and returns the final HTTP Request without a body +-/ +def build (builder : Builder) : Request Body := + { head := builder.head, body := .zero } + +/-- +Builds and returns the final HTTP Request with the specified body as binary data +-/ +def binary (builder : Builder) (bytes : ByteArray) : Request Body := + builder + |>.header "Content-Type" (.new "application/octet-stream") + |>.body (Body.bytes bytes) + +/-- +Builds and returns the final HTTP Request with the specified body as plain text +-/ +def text (builder : Builder) (body : String) : Request Body := + builder + |>.header "Content-Type" (.new "text/plain; charset=utf-8") + |>.body (body.toUTF8 |> Body.bytes) + +/-- +Builds and returns the final HTTP Request with the specified body as HTML +-/ +def html (builder : Builder) (body : String) : Request Body := + builder + |>.header "Content-Type" (.new "text/html; charset=utf-8") + |>.body (body.toUTF8 |> Body.bytes) + +end Builder + +/-- +Creates a new HTTP GET Request with the specified URI +-/ +def get (uri : RequestTarget) : Request Body := + new + |>.method .get + |>.uri uri + |>.build + +/-- +Creates a new HTTP POST Request with the specified URI and body +-/ +def post (uri : RequestTarget) (body : t) : Request t := + new + |>.method .post + |>.uri uri + |>.body body + +/-- +Creates a new HTTP PUT Request with the specified URI and body +-/ +def put (uri : RequestTarget) (body : t) : Request t := + new + |>.method .put + |>.uri uri + |>.body body + +/-- +Creates a new HTTP DELETE Request with the specified URI +-/ +def delete (uri : RequestTarget) : Request Body := + new + |>.method .delete + |>.uri uri + |>.build + +/-- +Creates a new HTTP PATCH Request with the specified URI and body +-/ +def patch (uri : RequestTarget) (body : t) : Request t := + new + |>.method .patch + |>.uri uri + |>.body body + +end Request diff --git a/src/Std/Internal/Http/Data/Response.lean b/src/Std/Internal/Http/Data/Response.lean new file mode 100644 index 000000000000..b11f06790558 --- /dev/null +++ b/src/Std/Internal/Http/Data/Response.lean @@ -0,0 +1,186 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Encode +public import Std.Internal.Http.Data.Body +public import Std.Internal.Http.Data.Status +public import Std.Internal.Http.Data.Headers +public import Std.Internal.Http.Data.Version + +public section + +namespace Std +namespace Http + +set_option linter.all true + +open Util +open Lean + +/-- +The main parts of a response. +-/ +structure Response.Head where + /-- + The HTTP status code and reason phrase, indicating the result of the request. + For example, `.ok` corresponds to `200 OK`. + -/ + status : Status := .ok + + /-- + The HTTP protocol version used in the response, e.g. `HTTP/1.1`. + -/ + version : Version := .v11 + + /-- + The set of response headers, providing metadata such as `Content-Type`, + `Content-Length`, and caching directives. + -/ + headers : Headers := .empty +deriving Inhabited, Repr + +/-- +HTTP response structure parameterized by body type +-/ +structure Response (t : Type) where + /-- + The information of the status-line of the request. + -/ + head : Response.Head := {} + + /-- + The content of the request. + -/ + body : Option t +deriving Inhabited + +/-- +Builds a HTTP Response. +-/ +structure Response.Builder where + /-- + The information of the status-line of the request. + -/ + head : Head := {} + +namespace Response + +instance : ToString Head where + toString r := + toString r.version ++ " " ++ + toString r.status.toCode ++ " " ++ + toString r.status ++ "\r\n" ++ + toString r.headers ++ "\r\n\r\n" + +/-- +Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1, empty headers) +-/ +def new : Builder := { } + +namespace Builder + +/-- +Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1, empty headers) +-/ +def empty : Builder := { } + +/-- +Sets the HTTP status code for the response being built +-/ +def status (builder : Builder) (status : Status) : Builder := + { builder with head := { builder.head with status := status } } + +/-- +Sets the HTTP version for the response being built +-/ +def version (builder : Builder) (version : Version) : Builder := + { builder with head := { builder.head with version := version } } + +/-- +Adds a single header to the response being built +-/ +def header (builder : Builder) (key : String) (value : HeaderValue) : Builder := + { builder with head := { builder.head with headers := builder.head.headers.insert key value } } + +/-- +Builds and returns the final HTTP Response with the specified body +-/ +def body (builder : Builder) (body : t) : Response t := + { head := builder.head, body := some body } + +/-- +Builds and returns the final HTTP Response. +-/ +def build (builder : Builder) : Response t := + { head := builder.head, body := none } + +/-- +Builds and returns the final HTTP Response with the specified body as binary data. +-/ +def binary (builder : Builder) (bytes : ByteArray) : Response Body := + builder + |>.header "Content-Type" (.new "application/octet-stream") + |>.body (Body.bytes bytes) + +/-- +Builds and returns the final HTTP Response with the specified body as plain text. +-/ +def text (builder : Builder) (body : String) : Response Body := + builder + |>.header "Content-Type" (.new "text/plain; charset=utf-8") + |>.body (body.toUTF8 |> Body.bytes) + +/-- +Builds and returns the final HTTP Response with the specified body as HTML. +-/ +def html (builder : Builder) (body : String) : Response Body := + builder + |>.header "Content-Type" (.new "text/html; charset=utf-8") + |>.body (body.toUTF8 |> Body.bytes) + +end Builder + +/-- +Creates a new HTTP Response with OK status and the provided string body +-/ +def ok (body : t) : Response t := + new.body body + +/-- +Creates a new HTTP Response with the specified status and string body +-/ +def buildWithStatus (status : Status) (body : t) : Response t := + new + |>.status status + |>.body body + +/-- +Convenience function to create a simple HTTP 404 Not Found response +-/ +def notFound [Coe String t] (body : String := "Not Found") : Response t := + new + |>.status .notFound + |>.body body + +/-- +Convenience function to create a simple HTTP 500 Internal Server Error response +-/ +def internalServerError [Coe String t] (body : String := "Internal Server Error") : Response t := + new + |>.status .internalServerError + |>.body body + +/-- +Convenience function to create a simple HTTP 400 Bad Request response +-/ +def badRequest [Coe String t] (body : String := "Bad Request") : Response t := + new + |>.status .badRequest + |>.body body + +end Response diff --git a/src/Std/Internal/Http/Data/Status.lean b/src/Std/Internal/Http/Data/Status.lean new file mode 100644 index 000000000000..13d3a1478629 --- /dev/null +++ b/src/Std/Internal/Http/Data/Status.lean @@ -0,0 +1,598 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Encode + +public section + +namespace Std +namespace Http + +set_option linter.all true + +/-- +HTTP Status codes. Status codes are three-digit integer codes that describes the result of a +HTTP request. In this implementation we do not treat status code as extensible. + +* Reference: https://httpwg.org/specs/rfc9110.html#status.codes + -/ +inductive Status where + /-- + 100 Continue + -/ + | «continue» + + /-- + 101 Switching Protocols + -/ + | switchingProtocols + + /-- + 102 Processing + -/ + | processing + + /-- + 103 Early Hints + -/ + | earlyHints + + /-- + 200 OK + -/ + | ok + + /-- + 201 Created + -/ + | created + + /-- + 202 Accepted + -/ + | accepted + + /-- + 203 Non-Authoritative Information + -/ + | nonAuthoritativeInformation + + /-- + 204 No Content + -/ + | noContent + + /-- + 205 Reset Content + -/ + | resetContent + + /-- + 206 Partial Content + -/ + | partialContent + + /-- + 207 Multi-Status + -/ + | multiStatus + + /-- + 208 Already Reported + -/ + | alreadyReported + + /-- + 226 IM Used + -/ + | imUsed + + /-- + 300 Multiple Choices + -/ + | multipleChoices + + /-- + 301 Moved Permanently + -/ + | movedPermanently + + /-- + 302 Found + -/ + | found + + /-- + 303 See Other + -/ + | seeOther + + /-- + 304 Not Modified + -/ + | notModified + + /-- + 305 Use Proxy + -/ + | useProxy + + /-- + 306 Unused + -/ + | unused + + /-- + 307 Temporary Redirect + -/ + | temporaryRedirect + + /-- + 308 Permanent Redirect + -/ + | permanentRedirect + + /-- + 400 Bad Request + -/ + | badRequest + + /-- + 401 Unauthorized + -/ + | unauthorized + + /-- + 402 Payment Required + -/ + | paymentRequired + + /-- + 403 Forbidden + -/ + | forbidden + + /-- + 404 Not Found + -/ + | notFound + + /-- + 405 Method Not Allowed + -/ + | methodNotAllowed + + /-- + 406 Not Acceptable + -/ + | notAcceptable + + /-- + 407 Proxy Authentication Required + -/ + | proxyAuthenticationRequired + + /-- + 408 Request Timeout + -/ + | requestTimeout + + /-- + 409 Conflict + -/ + | conflict + + /-- + 410 Gone + -/ + | gone + + /-- + 411 Length Required + -/ + | lengthRequired + + /-- + 412 Precondition Failed + -/ + | preconditionFailed + + /-- + 413 Payload Too Large + -/ + | payloadTooLarge + + /-- + 414 URI Too Long + -/ + | uriTooLong + + /-- + 415 Unsupported Media Type + -/ + | unsupportedMediaType + + /-- + 416 Range Not Satisfiable + -/ + | rangeNotSatisfiable + + /-- + 417 Expectation Failed + -/ + | expectationFailed + + /-- + 418 I'm a teapot + -/ + | imATeapot + + /-- + 421 Misdirected Request + -/ + | misdirectedRequest + + /-- + 422 Unprocessable Entity + -/ + | unprocessableEntity + + /-- + 423 Locked + -/ + | locked + + /-- + 424 Failed Dependency + -/ + | failedDependency + + /-- + 425 Too Early + -/ + | tooEarly + + /-- + 426 Upgrade Required + -/ + | upgradeRequired + + /-- + 428 Precondition Required + -/ + | preconditionRequired + + /-- + 429 Too Many Requests + -/ + | tooManyRequests + + /-- + 431 Request Header Fields Too Large + -/ + | requestHeaderFieldsTooLarge + + /-- + 451 Unavailable For Legal Reasons + -/ + | unavailableForLegalReasons + + /-- + 500 Internal Server Error + -/ + | internalServerError + + /-- + 501 Not Implemented + -/ + | notImplemented + + /-- + 502 Bad Gateway + -/ + | badGateway + + /-- + 503 Service Unavailable + -/ + | serviceUnavailable + + /-- + 504 Gateway Timeout + -/ + | gatewayTimeout + + /-- + 505 HTTP Version Not Supported + -/ + | httpVersionNotSupported + + /-- + 506 Variant Also Negotiates + -/ + | variantAlsoNegotiates + + /-- + 507 Insufficient Storage + -/ + | insufficientStorage + + /-- + 508 Loop Detected + -/ + | loopDetected + + /-- + 510 Not Extended + -/ + | notExtended + + /-- + 511 Network Authentication Required + -/ + | networkAuthenticationRequired +deriving Repr, Inhabited, BEq + +instance : ToString Status where + toString + | .«continue» => "Continue" + | .switchingProtocols => "Switching Protocols" + | .processing => "Processing" + | .earlyHints => "Early Hints" + | .ok => "OK" + | .created => "Created" + | .accepted => "Accepted" + | .nonAuthoritativeInformation => "Non-Authoritative Information" + | .noContent => "No Content" + | .resetContent => "Reset Content" + | .partialContent => "Partial Content" + | .multiStatus => "Multi-Status" + | .alreadyReported => "Already Reported" + | .imUsed => "IM Used" + | .multipleChoices => "Multiple Choices" + | .movedPermanently => "Moved Permanently" + | .found => "Found" + | .seeOther => "See Other" + | .notModified => "Not Modified" + | .useProxy => "Use Proxy" + | .unused => "Unused" + | .temporaryRedirect => "Temporary Redirect" + | .permanentRedirect => "Permanent Redirect" + | .badRequest => "Bad Request" + | .unauthorized => "Unauthorized" + | .paymentRequired => "Payment Required" + | .forbidden => "Forbidden" + | .notFound => "Not Found" + | .methodNotAllowed => "Method Not Allowed" + | .notAcceptable => "Not Acceptable" + | .proxyAuthenticationRequired => "Proxy Authentication Required" + | .requestTimeout => "Request Timeout" + | .conflict => "Conflict" + | .gone => "Gone" + | .lengthRequired => "Length Required" + | .preconditionFailed => "Precondition Failed" + | .payloadTooLarge => "Request Entity Too Large" + | .uriTooLong => "Request URI Too Long" + | .unsupportedMediaType => "Unsupported Media Type" + | .rangeNotSatisfiable => "Requested Range Not Satisfiable" + | .expectationFailed => "Expectation Failed" + | .imATeapot => "I'm a teapot" + | .misdirectedRequest => "Misdirected Request" + | .unprocessableEntity => "Unprocessable Entity" + | .locked => "Locked" + | .failedDependency => "Failed Dependency" + | .tooEarly => "Too Early" + | .upgradeRequired => "Upgrade Required" + | .preconditionRequired => "Precondition Required" + | .tooManyRequests => "Too Many Requests" + | .requestHeaderFieldsTooLarge => "Request Header Fields Too Large" + | .unavailableForLegalReasons => "Unavailable For Legal Reasons" + | .internalServerError => "Internal Server Error" + | .notImplemented => "Not Implemented" + | .badGateway => "Bad Gateway" + | .serviceUnavailable => "Service Unavailable" + | .gatewayTimeout => "Gateway Timeout" + | .httpVersionNotSupported => "HTTP Version Not Supported" + | .variantAlsoNegotiates => "Variant Also Negotiates" + | .insufficientStorage => "Insufficient Storage" + | .loopDetected => "Loop Detected" + | .notExtended => "Not Extended" + | .networkAuthenticationRequired => "Network Authentication Required" + +namespace Status + +/-- +Convert a Status to a numeric code. This is useful for sending the status code in a response. +-/ +def toCode : Status -> UInt16 + | «continue» => 100 + | switchingProtocols => 101 + | processing => 102 + | earlyHints => 103 + | ok => 200 + | created => 201 + | accepted => 202 + | nonAuthoritativeInformation => 203 + | noContent => 204 + | resetContent => 205 + | partialContent => 206 + | multiStatus => 207 + | alreadyReported => 208 + | imUsed => 226 + | multipleChoices => 300 + | movedPermanently => 301 + | found => 302 + | seeOther => 303 + | notModified => 304 + | useProxy => 305 + | unused => 306 + | temporaryRedirect => 307 + | permanentRedirect => 308 + | badRequest => 400 + | unauthorized => 401 + | paymentRequired => 402 + | forbidden => 403 + | notFound => 404 + | methodNotAllowed => 405 + | notAcceptable => 406 + | proxyAuthenticationRequired => 407 + | requestTimeout => 408 + | conflict => 409 + | gone => 410 + | lengthRequired => 411 + | preconditionFailed => 412 + | payloadTooLarge => 413 + | uriTooLong => 414 + | unsupportedMediaType => 415 + | rangeNotSatisfiable => 416 + | expectationFailed => 417 + | imATeapot => 418 + | misdirectedRequest => 421 + | unprocessableEntity => 422 + | locked => 423 + | failedDependency => 424 + | tooEarly => 425 + | upgradeRequired => 426 + | preconditionRequired => 428 + | tooManyRequests => 429 + | requestHeaderFieldsTooLarge => 431 + | unavailableForLegalReasons => 451 + | internalServerError => 500 + | notImplemented => 501 + | badGateway => 502 + | serviceUnavailable => 503 + | gatewayTimeout => 504 + | httpVersionNotSupported => 505 + | variantAlsoNegotiates => 506 + | insufficientStorage => 507 + | loopDetected => 508 + | notExtended => 510 + | networkAuthenticationRequired => 511 + +/-- +Converts an `UInt16` to a `Status`. +-/ +def fromCode? : UInt16 → Option Status + | 100 => some «continue» + | 101 => some switchingProtocols + | 102 => some processing + | 103 => some earlyHints + | 200 => some ok + | 201 => some created + | 202 => some accepted + | 203 => some nonAuthoritativeInformation + | 204 => some noContent + | 205 => some resetContent + | 206 => some partialContent + | 207 => some multiStatus + | 208 => some alreadyReported + | 226 => some imUsed + | 300 => some multipleChoices + | 301 => some movedPermanently + | 302 => some found + | 303 => some seeOther + | 304 => some notModified + | 305 => some useProxy + | 306 => some unused + | 307 => some temporaryRedirect + | 308 => some permanentRedirect + | 400 => some badRequest + | 401 => some unauthorized + | 402 => some paymentRequired + | 403 => some forbidden + | 404 => some notFound + | 405 => some methodNotAllowed + | 406 => some notAcceptable + | 407 => some proxyAuthenticationRequired + | 408 => some requestTimeout + | 409 => some conflict + | 410 => some gone + | 411 => some lengthRequired + | 412 => some preconditionFailed + | 413 => some payloadTooLarge + | 414 => some uriTooLong + | 415 => some unsupportedMediaType + | 416 => some rangeNotSatisfiable + | 417 => some expectationFailed + | 418 => some imATeapot + | 421 => some misdirectedRequest + | 422 => some unprocessableEntity + | 423 => some locked + | 424 => some failedDependency + | 425 => some tooEarly + | 426 => some upgradeRequired + | 428 => some preconditionRequired + | 429 => some tooManyRequests + | 431 => some requestHeaderFieldsTooLarge + | 451 => some unavailableForLegalReasons + | 500 => some internalServerError + | 501 => some notImplemented + | 502 => some badGateway + | 503 => some serviceUnavailable + | 504 => some gatewayTimeout + | 505 => some httpVersionNotSupported + | 506 => some variantAlsoNegotiates + | 507 => some insufficientStorage + | 508 => some loopDetected + | 510 => some notExtended + | 511 => some networkAuthenticationRequired + | _ => none + +/-- +Checks if the type of the status code is informational, meaning that the request was received +and the process is continuing. +-/ +@[inline] +def isInformational (c : Status) : Bool := + c.toCode < 200 + +/-- +Checks if the type of the status code is success, meaning that the request was successfully received, +understood, and accepted. + +* Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isSuccess (c : Status) : Bool := + 200 ≤ c.toCode ∧ c.toCode < 300 + +/-- +Checks if the type of the status code is redirection, meaning that further action needs to be taken +to complete the request. + +* Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isRedirection (c : Status) : Bool := + 300 ≤ c.toCode ∧ c.toCode < 400 + +/-- +Checks if the type of the status code is a client error, meaning that the request contains bad syntax +or cannot be fulfilled. + +* Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isClientError (c : Status) : Bool := + 400 ≤ c.toCode ∧ c.toCode < 500 + +/-- +Checks if the type of the status code is a server error, meaning that the server failed to fulfill +an apparently valid request. + +* Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isServerError (c : Status) : Bool := + 500 ≤ c.toCode ∧ c.toCode < 600 + +instance : Encode .v11 Status where + encode buffer status := buffer + |>.writeString (toString <| toCode status) + |>.writeChar ' ' + |>.writeString (toString status) diff --git a/src/Std/Internal/Http/Data/URI.lean b/src/Std/Internal/Http/Data/URI.lean new file mode 100644 index 000000000000..ab0e61c6d399 --- /dev/null +++ b/src/Std/Internal/Http/Data/URI.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Encode +public import Std.Internal.Http.Data.URI.Basic +public import Std.Internal.Http.Data.URI.Parser + +public section + +namespace Std +namespace Http +namespace RequestTarget + +set_option linter.all true + +/-- +Attempt to parse a `RequestTarget` from the given string. +-/ +@[inline] +def parse? (string : String) : Option RequestTarget := + Parser.parseRequestTarget.run string.toUTF8 |>.toOption + +/-- +Parse a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?` +if you need a safe option-returning version. +-/ +@[inline] +def parse! (string : String) : RequestTarget := + parse? string |>.get! diff --git a/src/Std/Internal/Http/Data/URI/Basic.lean b/src/Std/Internal/Http/Data/URI/Basic.lean new file mode 100644 index 000000000000..57feb3eb879e --- /dev/null +++ b/src/Std/Internal/Http/Data/URI/Basic.lean @@ -0,0 +1,302 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Net +public import Std.Internal.Http.Encode + +public section + +namespace Std +namespace Http + +set_option linter.all true + +namespace URI + +/-- +URI scheme (e.g., "http", "https", "ftp"). +-/ +abbrev Scheme := String + +/-- +User information component that usually contains the username and password. +-/ +abbrev UserInfo := String + +/-- +Host component of a URI, supporting domain names and IP addresses. +-/ +inductive Host + /-- + A registered name (typically a domain name). + -/ + | name (name : String) + + /-- + An IPv4 address. + -/ + | ipv4 (ipv4 : Net.IPv4Addr) + + /-- + An IPv6 address. + -/ + | ipv6 (ipv6 : Net.IPv6Addr) +deriving Inhabited + +instance : Repr Host where + reprPrec x prec := + let nestPrec := (if prec ≥ 1024 then 1 else 2) + let name := "Std.Http.URI.Host" + + let repr (ctr : String) a := + Repr.addAppParen (Format.nest nestPrec (.text s!"{name}.{ctr}" ++ .line ++ a)).group prec + + match x with + | Host.name a => repr "name" (reprArg a) + | Host.ipv4 a => repr "ipv4" (toString a) + | Host.ipv6 a => repr "ipv6" (toString a) + +/-- +TCP number port. +-/ +abbrev Port := UInt16 + +/-- +The authority component in a URI provides the necessary information for locating the resource +on the network. + +* Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2 +-/ +structure Authority where + /-- + Optional user information like user and password. + -/ + userInfo: Option UserInfo := none + + /-- + The host identifying the network location of the resource. + -/ + host: Host + + /-- + Optional port number for connecting to the host. + -/ + port: Option Port := none +deriving Inhabited, Repr + +/-- +Abstraction of paths. +-/ +structure Path where + /-- + Path segments making up the hierarchical structure. + -/ + segments : Array String + + /-- + Whether the path is absolute (begins with a `/`) or relative. + -/ + absolute : Bool := false +deriving Inhabited, Repr + +/-- +Query string represented as an array of key–value pairs. +-/ +@[expose] +def Query := Array (String × Option String) + +instance : Repr Query := + inferInstanceAs (Repr (Array (String × Option String))) + +end URI + +/-- +Complete URI structure following RFC 3986. +-/ +structure URI where + /-- + The scheme of the URI (e.g., "http", "https", "ftp"). + -/ + scheme : URI.Scheme + + /-- + Optional authority component containing user info, host, and port. + -/ + authority : Option URI.Authority + + /-- + Path component of the URI, representing the hierarchical location. + -/ + path : URI.Path + + /-- + Optional query string of the URI represented as key–value pairs. + -/ + query : Option URI.Query + + /-- + Optional fragment identifier of the URI (the part after `#`). + -/ + fragment : Option String +deriving Inhabited, Repr + +/-- +HTTP request target forms as defined in RFC 7230 Section 5.3. +-/ +inductive RequestTarget where + /-- + Request target using an origin-form (most common form for HTTP requests), + consisting of a path, an optional query string, and an optional fragment. + -/ + | originForm (path : URI.Path) (query : Option URI.Query) (fragment : Option String) + + /-- + Request target using an absolute-form URI. + -/ + | absoluteForm (uri : URI) + + /-- + Request target using the authority-form, typically for CONNECT requests. + -/ + | authorityForm (authority : URI.Authority) + + /-- + Asterisk-form request target, typically used with OPTIONS requests. + -/ + | asteriskForm +deriving Inhabited, Repr + +namespace RequestTarget + +/-- +Returns the path component of a `RequestTarget`, if available. +-/ +def path? : RequestTarget → Option URI.Path + | .originForm p _ _ => some p + | .absoluteForm u => some u.path + | _ => none + +/-- +Returns the query component of a `RequestTarget`, if available. +-/ +def query? : RequestTarget → Option URI.Query + | .originForm _ q _ => q + | .absoluteForm u => u.query + | _ => none + +/-- +Returns the authority component of a `RequestTarget`, if available. +-/ +def authority? : RequestTarget → Option URI.Authority + | .authorityForm a => some a + | .absoluteForm u => u.authority + | _ => none + +/-- +Returns the full URI if the `RequestTarget` is in absolute form, otherwise `none`. +-/ +def uri? : RequestTarget → Option URI + | .absoluteForm u => some u + | _ => none + +end RequestTarget + +-- ToString implementations + +private def isUnreserved (c : UInt8) : Bool := + (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) || (c ≥ 'a'.toUInt8 && c ≤ 'z'.toUInt8) || (c ≥ 'A'.toUInt8 && c ≤ 'Z'.toUInt8) + || c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8 + +private def hexDigit (n : UInt8) : UInt8 := + if n < 10 then (n + '0'.toUInt8) + else (n - 10 + 'A'.toUInt8) + +private def byteToHex (b : UInt8) : ByteArray := + let hi := hexDigit (b >>> 4) + let lo := hexDigit (b &&& 0xF) + ByteArray.mk #['%'.toUInt8, hi, lo] + +/-- +Encodes a string as a URI component by percent-encoding all characters +--/ +def encodeURIComponent (s : String) : ByteArray := + s.toUTF8.foldl (init := ByteArray.emptyWithCapacity s.utf8ByteSize) fun acc c => + if isUnreserved c then acc.push c else acc.append (byteToHex c) + +instance : ToString URI.Host where + toString + | .name n => String.fromUTF8! (encodeURIComponent n) + | .ipv4 addr => toString addr + | .ipv6 addr => s!"[{toString addr}]" + +instance : ToString URI.Authority where + toString auth := + let userPart := match auth.userInfo with + | none => "" + | some ui => s!"{encodeURIComponent ui}@" + let hostPart := toString auth.host + let portPart := match auth.port with + | none => "" + | some p => s!":{p}" + s!"{userPart}{hostPart}{portPart}" + +instance : ToString URI.Path where + toString + | ⟨segs, abs⟩ => + let encodedSegs := segs.toList.map (fun seg => String.fromUTF8! (encodeURIComponent seg)) + let core := String.intercalate "/" encodedSegs + if abs then s!"/{core}" else core + +/-- +? +-/ +def encodeQueryParam (key : String) (value : Option String) : String := + let encodedKey := String.fromUTF8! (encodeURIComponent key) + match value with + | none => encodedKey + | some v => + let encodedValue := String.fromUTF8! (encodeURIComponent v) + s!"{encodedKey}={encodedValue}" + +instance : ToString URI.Query where + toString q := + if q.isEmpty then "" else + let encodedParams := q.toList.map fun (key, value) => + match key with + | "" => match value with + | none => "" + | some v => s!"={String.fromUTF8! (encodeURIComponent v)}" + | k => encodeQueryParam k value + "?" ++ String.intercalate "&" encodedParams + +instance : ToString URI where + toString uri := + let schemePart := String.fromUTF8! (encodeURIComponent uri.scheme) + let authorityPart := match uri.authority with + | none => "" + | some auth => s!"//{toString auth}" + let pathPart := toString uri.path + let queryPart := uri.query.map toString |>.getD "" + let fragmentPart := match uri.fragment with + | none => "" + | some f => s!"#{String.fromUTF8! (encodeURIComponent f)}" + s!"{schemePart}{authorityPart}{pathPart}{queryPart}{fragmentPart}" + +instance : ToString RequestTarget where + toString + | .originForm path query frag => + let pathStr := toString path + let queryStr := query.map toString |>.getD "" + let frag := frag.map ("#" ++ ·) |>.getD "" + s!"{pathStr}{queryStr}{frag}" + | .absoluteForm uri => toString uri + | .authorityForm auth => toString auth + | .asteriskForm => "*" + +end Http +end Std diff --git a/src/Std/Internal/Http/Data/URI/Parser.lean b/src/Std/Internal/Http/Data/URI/Parser.lean new file mode 100644 index 000000000000..1ef51defa9eb --- /dev/null +++ b/src/Std/Internal/Http/Data/URI/Parser.lean @@ -0,0 +1,339 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Parsec +public import Std.Internal.Parsec.ByteArray +public import Std.Internal.Http.Data.URI.Basic + +public section + +namespace Std +namespace Http +namespace Parser + +set_option linter.all true + +open Std Internal Parsec ByteArray + +@[inline] +private def isDigit (c : UInt8) : Bool := + c >= '0'.toUInt8 ∧ c <= '9'.toUInt8 + +@[inline] +private def isHexDigit (c : UInt8) : Bool := + isDigit c ∨ (c >= 'A'.toUInt8 ∧ c <= 'F'.toUInt8) ∨ (c >= 'a'.toUInt8 ∧ c <= 'f'.toUInt8) + +@[inline] +private def isAlpha (c : UInt8) : Bool := + (c >= 'A'.toUInt8 ∧ c <= 'Z'.toUInt8) ∨ (c >= 'a'.toUInt8 ∧ c <= 'z'.toUInt8) + +@[inline] +private def isAlphaNum (c : UInt8) : Bool := + isAlpha c ∨ isDigit c + +@[inline] +private def isUnreserved (c : UInt8) : Bool := + isAlphaNum c ∨ c = '-'.toUInt8 ∨ c = '.'.toUInt8 ∨ c = '_'.toUInt8 ∨ c = '~'.toUInt8 + +@[inline] +private def isSubDelims (c : UInt8) : Bool := + c = '!'.toUInt8 ∨ c = '$'.toUInt8 ∨ c = '&'.toUInt8 ∨ c = '\''.toUInt8 ∨ + c = '('.toUInt8 ∨ c = ')'.toUInt8 ∨ c = '*'.toUInt8 ∨ c = '+'.toUInt8 ∨ + c = ','.toUInt8 ∨ c = ';'.toUInt8 ∨ c = '='.toUInt8 + +@[inline] +private def isGenDelims (c : UInt8) : Bool := + c = ':'.toUInt8 ∨ c = '/'.toUInt8 ∨ c = '?'.toUInt8 ∨ c = '#'.toUInt8 ∨ + c = '['.toUInt8 ∨ c = ']'.toUInt8 ∨ c = '@'.toUInt8 + +@[inline] +private def isReserved (c : UInt8) : Bool := + isGenDelims c ∨ isSubDelims c + +@[inline] +private def isPChar (c : UInt8) : Bool := + isUnreserved c ∨ isSubDelims c ∨ c = ':'.toUInt8 ∨ c = '@'.toUInt8 ∨ c = '%'.toUInt8 + +@[inline] +private def isRegNameChar (c : UInt8) : Bool := + isUnreserved c ∨ isSubDelims c ∨ c = '%'.toUInt8 + +@[inline] +private def isSchemeChar (c : UInt8) : Bool := + isAlphaNum c ∨ c = '+'.toUInt8 ∨ c = '-'.toUInt8 ∨ c = '.'.toUInt8 + +@[inline] +private def isQueryChar (c : UInt8) : Bool := + isPChar c ∨ c = '/'.toUInt8 ∨ c = '?'.toUInt8 + +@[inline] +private def isFragmentChar (c : UInt8) : Bool := + isPChar c ∨ c = '/'.toUInt8 ∨ c = '?'.toUInt8 + +@[inline] +private def isUserInfoChar (c : UInt8) : Bool := + isUnreserved c ∨ isSubDelims c ∨ c = '%'.toUInt8 ∨ c = ':'.toUInt8 + +@[inline] +private def tryOpt (p : Parser α) : Parser (Option α) := + optional (attempt p) + +@[inline] +private def ofExcept (p : Except String α) : Parser α := + match p with + | .ok res => pure res + | .error err => fail err + +@[inline] +private def peekIs (p : UInt8 → Bool) : Parser Bool := do + return (← peekWhen? p).isSome + +private def hexToByte (digit : UInt8) : UInt8 := + if digit <= '9'.toUInt8 then digit - '0'.toUInt8 + else if digit <= 'F'.toUInt8 then digit - 'A'.toUInt8 + 10 + else digit - 'a'.toUInt8 + 10 + +private def hexToByte? (digit : UInt8) : Option UInt8 := + if digit ≥ '0'.toUInt8 ∧ digit ≤ '9'.toUInt8 then some (digit - '0'.toUInt8) + else if digit ≥ 'A'.toUInt8 ∧ digit ≤ 'F'.toUInt8 then some (digit - 'A'.toUInt8 + 10) + else if digit ≥ 'a'.toUInt8 ∧ digit ≤ 'f'.toUInt8 then some (digit - 'a'.toUInt8 + 10) + else none + +private def parsePctEncoded : Parser UInt8 := do + skipByte '%'.toUInt8 + let hi ← hexToByte <$> satisfy isHexDigit + let lo ← hexToByte <$> satisfy isHexDigit + return (hi <<< 4) ||| lo + +/-- +Decode a percent encoded byte array to an extended ascii string. +-/ +public partial def percentDecode (ba : ByteArray) : Except String String := do + let rec loop (i : Nat) (acc : ByteArray) : Except String ByteArray := + if i ≥ ba.size then + .ok acc + else + let c := ba.get! i + if c = '%'.toUInt8 then + if i + 2 ≥ ba.size then + Except.error "invalid percent encoding" + else + match hexToByte? (ba.get! (i+1)), hexToByte? (ba.get! (i+2)) with + | some hi, some lo => loop (i + 3) (acc.push ((hi <<< 4) ||| lo)) + | _, _ => .error "cannot get values" + else + loop (i + 1) (acc.push c) + + let result ← loop 0 .empty + match String.fromUTF8? result with + | some res => .ok res + | none => Except.error "invalid percent encoding" + +-- scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." ) +private def parseScheme : Parser URI.Scheme := do + let schemeBytes ← takeWhileUpTo1 isSchemeChar 63 + return String.fromUTF8! schemeBytes.toByteArray + +-- port = *DIGIT +private def parsePortNumber : Parser UInt16 := do + let portBytes ← takeWhileUpTo isDigit 5 + if portBytes.size = 0 then fail "empty port number" + let portStr := String.fromUTF8! portBytes.toByteArray + + let some portNum := String.toNat? portStr + | fail s!"invalid port number: {portStr}" + + if portNum > 65535 then + fail s!"port number too large: {portNum}" + + return portNum.toUInt16 + +-- userinfo = *( unreserved / pct-encoded / sub-delims / ":" ) +private def parseUserInfo : Parser URI.UserInfo := do + let userBytes ← takeWhileUpTo isUserInfoChar 1024 + + let .ok userStr := percentDecode userBytes.toByteArray + | fail "invalid percent encoding in user info" + + return userStr + +-- IP-literal = "[" ( IPv6address / IPvFuture ) "]" +private def parseIPv6 : Parser Net.IPv6Addr := do + skipByte '['.toUInt8 + + let result ← takeWhileUpTo1 (fun x => x = ':'.toUInt8 ∨ isHexDigit x) 256 + + skipByte ']'.toUInt8 + + let ipv6Str := String.fromUTF8! result.toByteArray + let some ipv6Addr := Std.Net.IPv6Addr.ofString ipv6Str + | fail s!"invalid IPv6 address: {ipv6Str}" + + return ipv6Addr + +-- IPv4address = dec-octet "." dec-octet "." dec-octet "." dec-octet +private def parseIPv4 : Parser Net.IPv4Addr := do + let result ← takeWhileUpTo1 (fun x => x = '.'.toUInt8 ∨ isDigit x) 256 + + let ipv4Str := String.fromUTF8! result.toByteArray + let some ipv4Str := Std.Net.IPv4Addr.ofString ipv4Str + | fail s!"invalid IPv4 address: {ipv4Str}" + + return ipv4Str + +-- host = IP-literal / IPv4address / reg-name +private def parseHost : Parser URI.Host := do + if (← peekWhen? (· == '['.toUInt8)).isSome then + return .ipv6 (← parseIPv6) + else if (← peekWhen? isDigit).isSome then + return .ipv4 (← parseIPv4) + else + let isHostName x := isUnreserved x ∨ x = '%'.toUInt8 ∨ isSubDelims x + let str ← ofExcept <| percentDecode (← takeWhileUpTo1 isHostName 1024).toByteArray + return .name str + +-- authority = [ userinfo "@" ] host [ ":" port ] +private def parseAuthority : Parser URI.Authority := do + let userinfo ← tryOpt do + let ui ← parseUserInfo + skipByte '@'.toUInt8 + return ui + + let host ← parseHost + + let port ← optional do + skipByte ':'.toUInt8 + parsePortNumber + + return { userInfo := userinfo, host := host, port := port } + +-- segment = *pchar +private def parseSegment : Parser ByteSlice := do + takeWhileUpTo isPChar 256 + +/-- +path = path-abempty ; begins with "/" or is empty + / path-absolute ; begins with "/" but not "//" + / path-noscheme ; begins with a non-colon segment + / path-rootless ; begins with a segment + / path-empty ; zero characters + +path-abempty = *( "/" segment ) +path-absolute = "/" [ segment-nz *( "/" segment ) ] +path-noscheme = segment-nz-nc *( "/" segment ) +path-rootless = segment-nz *( "/" segment ) +path-empty = 0 +-/ + +private def parsePath (forceAbsolute : Bool) : Parser URI.Path := do + let mut isAbsolute := false + let mut segments : Array String := #[] + + -- Check if path is absolute + if ← peekIs (· == '/'.toUInt8) then + isAbsolute := true + skip + if ← peekIs (· == '/'.toUInt8) then + fail "it's a scheme starter" + else if forceAbsolute then + fail "require '/' in path" + else + pure () + -- Parse segments + while true do + let segmentBytes ← parseSegment + + let .ok segmentStr := percentDecode segmentBytes.toByteArray + | fail "invalid percent encoding in path segment" + + segments := segments.push segmentStr + + if (← peek?).any (· == '/'.toUInt8) then + skip + else + break + + return { segments := segments, absolute := isAbsolute } + + +-- query = *( pchar / "/" / "?" ) +private def parseQuery : Parser URI.Query := do + let queryBytes ← takeWhileUpTo isQueryChar 1024 + let queryStr := String.fromUTF8! queryBytes.toByteArray + + let pairs ← queryStr.splitOn "&" |>.mapM fun pair => do + match pair.splitOn "=" with + | [key] => + let .ok decodedKey := percentDecode key.toUTF8 + | fail "invalid percent encoding in query key" + pure (decodedKey, none) + | key :: value => + let .ok decodedKey := percentDecode key.toUTF8 + | fail "invalid percent encoding in query key" + let .ok decodedValue := percentDecode (String.intercalate "=" value).toUTF8 + | fail "invalid percent encoding in query value" + pure (decodedKey, some decodedValue) + | [] => pure ("", none) + + return pairs.toArray + +-- fragment = *( pchar / "/" / "?" ) +private def parseFragment : Parser String := do + let fragmentBytes ← takeWhileUpTo isFragmentChar 1024 + + let .ok fragmentStr := percentDecode fragmentBytes.toByteArray + | fail "invalid percent encoding in fragment" + + return fragmentStr + +/-- +Parses a request target with combined parsing and validation. +-/ +public def parseRequestTarget : Parser RequestTarget := do + + -- The asterisk form + if (← tryOpt (skipByte '*'.toUInt8)).isSome then + return .asteriskForm + + -- origin-form = absolute-path [ "?" query ] + -- absolute-path = 1*( "/" segment ) + if ← peekIs (· == '/'.toUInt8) then + let path ← parsePath false + let query ← optional (skipByte '?'.toUInt8 *> parseQuery) + let frag ← optional (skipByte '#'.toUInt8 *> parseFragment) + return .originForm path query frag + + let authorityForm ← tryOpt do + let host ← parseHost + skipByteChar ':' + let port ← parsePortNumber + return RequestTarget.authorityForm { host, port := some port } + + -- absolute-URI = scheme ":" hier-part [ "?" query ] + let scheme ← tryOpt do + let scheme ← parseScheme + skipByte ':'.toUInt8 + return scheme + + if let some authorityForm := authorityForm then + return authorityForm + + -- absolute-URI = scheme ":" hier-part [ "?" query ] + if let some scheme := scheme then + -- hier-part = "//" authority path-abempty + let authority ← optional (skipString "//" *> parseAuthority) + let path ← parsePath true + let query ← optional (skipByteChar '?' *> parseQuery) + let fragment ← optional (skipByteChar '#' *> parseFragment) + return .absoluteForm { path, scheme, authority, query, fragment } + + fail "invalid request target" + +end Parser +end Http +end Std diff --git a/src/Std/Internal/Http/Data/Version.lean b/src/Std/Internal/Http/Data/Version.lean new file mode 100644 index 000000000000..f104de134a65 --- /dev/null +++ b/src/Std/Internal/Http/Data/Version.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.String + +public section + +namespace Std +namespace Http + +set_option linter.all true + +/-- +The 'Version' structure represents an HTTP version with a major and minor number. It includes +several standard versions of the HTTP protocol, such as HTTP/1.1, HTTP/2.0, and +HTTP/3.0. + +* Reference: https://httpwg.org/specs/rfc9110.html#protocol.version +-/ +inductive Version + + /-- + `HTTP/1.1` + -/ + | v11 + + /-- + `HTTP/2.0` + -/ + | v20 + + /-- + `HTTP/3.0` + -/ + | v30 + +deriving Repr, Inhabited, BEq, DecidableEq + +namespace Version + +/-- +Converts a pair of `Nat` to the corresponding `Version`. +-/ +def fromNumber? : Nat → Nat → Option Version + | 1, 1 => some .v11 + | 2, 0 => some .v20 + | 3, 0 => some .v30 + | _, _ => none + +/-- +Converts `String` to the corresponding `Version`. +-/ +def fromString? : String → Option Version + | "HTTP/1.1" => some .v11 + | "HTTP/2.0" => some .v20 + | "HTTP/3.0" => some .v30 + | _ => none + +/-- +Converts a `Version` to its corresponding major and minor numbers as a pair. +-/ +def toNumber : Version → (Nat × Nat) + | .v11 => (1, 1) + | .v20 => (2, 0) + | .v30 => (3, 0) + +instance : ToString Version where + toString + | .v11 => "HTTP/1.1" + | .v20 => "HTTP/2.0" + | .v30 => "HTTP/3.0" diff --git a/src/Std/Internal/Http/Encode.lean b/src/Std/Internal/Http/Encode.lean new file mode 100644 index 000000000000..4b1101a19671 --- /dev/null +++ b/src/Std/Internal/Http/Encode.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Util.Buffer +public import Std.Internal.Http.Data.Version + +public section + +namespace Std +namespace Http + +open Util + +set_option linter.all true + +/-- +Serializes a type `t` to a `Buffer` containing its canonical HTTP representation +for protocol version `v`. +-/ +class Encode (v : Version) (t : Type) where + /-- + Encodes a type `t` to a `Buffer`. + -/ + encode : Buffer → t → Buffer + +instance : Encode .v11 Version where + encode buffer := buffer.writeString ∘ toString diff --git a/src/Std/Internal/Http/Protocol/H1.lean b/src/Std/Internal/Http/Protocol/H1.lean new file mode 100644 index 000000000000..907b44027f8b --- /dev/null +++ b/src/Std/Internal/Http/Protocol/H1.lean @@ -0,0 +1,929 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Time +public import Std.Internal.Http.Data +public import Std.Internal.Http.Util +public import Std.Internal.Http.Protocol.H1.Parser + +public section + +namespace Std +namespace Http +namespace Protocol +namespace H1 + +open Std Internal Parsec ByteArray +open Util + +namespace Machine + +/-- +Connection limits configuration with validation. +-/ +structure Config where + /-- + Maximum number of requests per connection. + -/ + maxRequests : Nat := 100 + + /-- + Maximum number of headers allowed per request. + -/ + maxHeaders : Nat := 50 + + /-- + Maximum size of a single header value. + -/ + maxHeaderSize : Nat := 8192 + + /-- + Whether to enable keep-alive connections by default. + -/ + enableKeepAlive : Bool := true + + /-- + Size threshold for flushing output buffer. + -/ + highMark : Nat := 4096 + + /-- + The server name + -/ + serverName : Option HeaderValue := some (.new "LeanHTTP/1.1") + +/-- +Specific HTTP processing errors with detailed information. +-/ +inductive Error + /-- + Malformed request line or status line. + -/ + | invalidStatusLine + + /-- + Invalid or malformed header. + -/ + | invalidHeader + + /-- + Request timeout occurred. + -/ + | timeout + + /-- + Request entity too large. + -/ + | entityTooLarge + + /-- + Unsupported HTTP method. + -/ + | unsupportedMethod + + /-- + Unsupported HTTP version. + -/ + | unsupportedVersion + + /-- + Invalid chunk encoding. + -/ + | invalidChunk + + /-- + Bad request + -/ + | badRequest + + /-- + Generic error with message. + -/ + | other (message : String) +deriving Repr, BEq + +instance : Repr ByteSlice where + reprPrec x := reprPrec x.toByteArray.data + +/-- +Events that can occur during HTTP message processing. +-/ +inductive Event + /-- + Event received when chunk extension data is encountered in chunked encoding. + -/ + | chunkExt (ext : Array (String × Option String)) + + /-- + Event received the headers end. + -/ + | endHeaders (size : Request.Head) + + /-- + Event received when some data arrives from the received thing. + -/ + | gotData (final : Bool) (data : ByteSlice) + + /-- + Need more data is an event that arrives when the input ended and it requires more + data to continue + -/ + | needMoreData (size : Option Nat) + + /-- + Event received when parsing or processing fails with an error message. + -/ + | failed + + /-- + Event received when connection should be closed. + -/ + | close + + /-- + Awaiting the next request + -/ + | next +deriving Inhabited, Repr + +inductive Reader.State : Type + /-- + Initial state waiting for HTTP start line. + -/ + | needStartLine : State + + /-- + State waiting for HTTP headers, tracking number of headers parsed. + -/ + | needHeader : Nat → State + + /-- + State waiting for chunk size in chunked transfer encoding. + -/ + | needChunkedSize : State + + /-- + State waiting for chunk body data of specified size. + -/ + | needChunkedBody : Nat → State + + /-- + State waiting for fixed-length body data of specified size. + -/ + | needFixedBody : Nat → State + + /-- + Requires the response to continue. + -/ + | requireResponse : Body.Length → State + + /-- + State when request is fully parsed and ready to generate response. + -/ + | complete : State + + /-- + The input is malformed. + -/ + | failed (error : Response.Head) : State +deriving Inhabited, Repr + +inductive Writer.State + /-- + Ready to write the response + -/ + | waitingHeaders + + /-- + This is the state that we wait for a forced flush. This happens and causes the writer to + start actually writing to the outputData + -/ + | waitingForFlush + + /-- + Writing the headers. + -/ + | writingHeaders + + /-- + Writing a fixed size body output. + -/ + | writingFixedData + + /-- + Writing chunked data. + -/ + | writingChunkedBody + + /-- + State when response is fully sent and ready to the next request. + -/ + | complete : State +deriving BEq, Repr + +/-- +Manages the reading state of the machine. +-/ +structure Reader where + /-- + The current state of the machine. + -/ + state : Machine.Reader.State := .needStartLine + + /-- + The input byte array. + -/ + input : ByteArray.Iterator := ByteArray.emptyWithCapacity 4096 |>.iter + + /-- + The request head. + -/ + request : Request.Head := {} + + /-- + Count of requests that this connection already parsed + -/ + requestCount : Nat := 0 + +namespace Reader + +@[inline] +def feed (data : ByteArray) (reader : Reader) : Reader := + { reader with input := + if reader.input.atEnd + then data.iter + else { reader.input with array := reader.input.array ++ data } } + +@[inline] +def setInput (input : ByteArray.Iterator) (reader : Reader) : Reader := + { reader with input } + +@[inline] +def setRequest (request : Request.Head) (reader : Reader) : Reader := + { reader with request } + +@[inline] +def addHeader (name : String) (value : HeaderValue) (reader : Reader) : Reader := + { reader with request := { reader.request with headers := reader.request.headers.insert name value } } + +end Reader + +/-- +Manages the writing state of the machine. +-/ +structure Writer where + /-- + This is all the data that the user is sending that is being accumulated. + -/ + userData : BufferBuilder := .empty + + /-- + The chunk headers that are going to be with the chunk + -/ + chunkExt : Array (Array (String × Option String)) := .empty + + /-- + All the data that is going to get out of the writer. + -/ + outputData : BufferBuilder := .empty + + /-- + The state of the writer machine. It carries if the reader had already read the headers, the size + of the output, if it's chunked or not. + -/ + state : Machine.Writer.State := .waitingHeaders + + /-- + When the user specifies the exact size upfront, we can use Content-Length + instead of chunked transfer encoding for streaming + -/ + knownSize : Option Nat := none + + /-- + The Response that will be written to the output + -/ + response : Response.Head := {} + + /-- + This flags that the writer is closed so if we start to write the body we know exactly the size. + -/ + closed : Bool := false + +namespace Writer + +/-- +Resets and closes the connection +-/ +def resetAndClose (writer : Writer) : Writer := + match writer.state with + | .waitingForFlush => + { writer with userData := .empty, closed := true } + | _ => + writer + +/-- +Close the writer, enabling size determination +--/ +@[inline] +def close (writer : Writer) : Writer := + { writer with closed := true } + +/-- +Set a known size for the response body, enabling streaming with Content-Length +-/ +@[inline] +def setKnownSize (size : Nat) (writer : Writer) : Writer := + { writer with knownSize := some size } + +/-- +Determine the body size based on writer state and closure +--/ +private def determineBodySize (writer : Writer) : Body.Length := + if let some size := writer.knownSize then + .fixed size + else if writer.closed then + .fixed writer.userData.size + else + .chunked + +/-- +Add data to the user data buffer +-/ +@[inline] +def addUserData (data : Util.BufferBuilder) (writer : Writer) : Writer := + if writer.closed then + writer + else + { writer with userData := writer.userData.append data } + +/-- +Add data to the user chunk ext buffer +-/ +@[inline] +def addChunkExt (data : Array (String × Option String)) (writer : Writer) : Writer := + if writer.closed then + writer + else + { writer with chunkExt := writer.chunkExt.push data } + +/-- +Write fixed-size body data +-/ +private def writeFixedBody (writer : Writer) : Writer := + if writer.userData.size = 0 then + writer + else + let data := writer.userData + { writer with + userData := BufferBuilder.empty + outputData := writer.outputData.append data + } + +/-- +Write fixed-size body data +-/ +private def writeChunkedBody (writer : Writer) : Writer := + if writer.userData.size = 0 then + writer + else + let data := writer.userData + + let ext : Array String := writer.chunkExt.take data.size |>.map (Array.foldl + (fun acc (name, value) => acc ++ ";" ++ name ++ (value.map (fun x => "=" ++ x) |>.getD "")) + "") + + let chunks := data.data.mapIdx fun idx ba => + let chunkLen := ba.size + let chunkHeader := + (Nat.toDigits 16 chunkLen |>.toArray |>.map Char.toUInt8 |> ByteArray.mk) + ++ (ext[idx]? |>.map String.toUTF8 |>.getD .empty) + ++ "\r\n".toUTF8 + chunkHeader ++ ba ++ "\r\n".toUTF8 + + { writer with + userData := BufferBuilder.empty + chunkExt := writer.chunkExt.drop data.size + outputData := writer.outputData ++ chunks + } + +private def writeFinalChunk (writer : Writer) : Writer := + let writer := writer.writeChunkedBody + + { writer with + outputData := writer.outputData.append "0\r\n\r\n".toUTF8 + state := .complete + } + +/-- +Get the current output data and clear the buffer +-/ +@[inline] +def takeOutput (writer : Writer) : Option (Writer × ByteArray) := + let output := writer.outputData.toByteArray + some ({ writer with outputData := BufferBuilder.empty }, output) + +/-- +Set the writer state +-/ +@[inline] +def setState (state : Machine.Writer.State) (writer : Writer) : Writer := + { writer with state } + +/-- +Write response headers to output buffer +-/ +private def writeHeaders (response : Response.Head) (writer : Writer) : Writer := + { writer with outputData := writer.outputData.push (toString response).toUTF8 } + +end Writer +end Machine + +/-- +The state machine that receives some input bytes and outputs bytes for the HTTP 1.1 protocol. +-/ +structure Machine where + /-- + The state of the reader. + -/ + reader : Machine.Reader := {} + + /-- + The state of the writer. + -/ + writer : Machine.Writer := {} + + /-- + The configuration of the machine. + -/ + config : Machine.Config := {} + + /-- + Events that happend during reading and writing. + -/ + events : Array Machine.Event := #[] + + /-- + Error thrown by the machine + -/ + error : Option Machine.Error := none + + /-- + The timestamp that will be used to create the `Date` header. + -/ + instant : Option (Std.Time.DateTime .UTC) := none + + /-- + If the request will be kept alive after the request. + -/ + keepAlive : Bool := false + +namespace Machine + +private def shouldBreakConnection (c : Status) : Bool := + match c with + | .uriTooLong + | .badRequest + | .payloadTooLarge + | .requestHeaderFieldsTooLarge => true + | _ => false + +-- Additional helper functions for writer manipulation +@[inline] +private def modifyWriter (machine : Machine) (fn : Writer → Writer) : Machine := + { machine with writer := fn machine.writer } + +@[inline] +private def resetAndClose (machine : Machine) : Machine := + machine.modifyWriter (·.resetAndClose) + +@[inline] +private def setWriterState (machine : Machine) (state : Writer.State) : Machine := + machine.modifyWriter ({ · with state }) + +@[inline] +private def addEvent (machine : Machine) (event : Event) : Machine := + { machine with events := machine.events.push event } + +@[inline] +private def setEvent (machine : Machine) (event : Option Event) : Machine := + match event with + | some event => machine.addEvent event + | none => machine + +@[inline] +private def setError (machine : Machine) (error : Machine.Error) : Machine := + { machine with error := some error } + +@[inline] +private def closeConnection (machine : Machine) : Machine := + { machine with keepAlive := false } + +@[inline] +private def modifyReader (machine : Machine) (fn : Reader → Reader) : Machine := + { machine with reader := fn machine.reader } + +@[inline] +private def setReaderState (machine : Machine) (state : Reader.State) : Machine := + machine.modifyReader ({ · with state }) + +@[inline] +def setFailure (machine : Machine) (error : H1.Machine.Error) (status : Status) : Machine := + machine + |>.addEvent .failed + |>.setReaderState (.failed { status }) + |>.setError error + +private def parseWith (machine : Machine) (parser : Parser α) (limit : Option Nat) (expect : Option Nat := none) : (Machine × Option α) := + let remaining := machine.reader.input.remainingBytes + match parser machine.reader.input with + | .success buffer reqLine => ({ machine with reader := machine.reader.setInput buffer }, some reqLine) + | .error it .eof => + let usedBytesUntilFailure := remaining - it.remainingBytes + + if let some limit := limit then + if usedBytesUntilFailure ≥ limit + then (machine.setFailure .badRequest .badRequest, none) + else (machine.addEvent (.needMoreData expect), none) + else (machine.addEvent (.needMoreData expect), none) + | .error _ _ => + (machine.setFailure .badRequest .badRequest, none) + +/-- +Set a known size for the response body +-/ +@[inline] +def setKnownSize (machine : Machine) (size : Nat) : Machine := + { machine with writer := machine.writer.setKnownSize size } + +/-- +Reset the machine for the next request after response is complete +-/ +private def resetForNextRequest (machine : Machine) : Machine := + let newRequestCount := machine.reader.requestCount + 1 + let shouldKeepAlive := machine.keepAlive && newRequestCount < machine.config.maxRequests + + if shouldKeepAlive then + { machine with + reader := { + state := .needStartLine, + input := machine.reader.input, + request := {}, + requestCount := newRequestCount + }, + writer := { + userData := .empty, + chunkExt := .empty, + outputData := machine.writer.outputData, + state := .waitingHeaders, + closed := false, + knownSize := none, + response := {}, + }, + events := machine.events.push .next, + error := none, + instant := none + } + else + machine.addEvent .close + +-- Validation of request + +private def determineKeepAlive (machine : Machine) : Bool := + let connectionHeader := machine.reader.request.headers.getLast? "Connection" |>.getD (.new "keep-alive") + let explicitClose := connectionHeader.is "close" + let explicitKeepAlive := connectionHeader.is "keep-alive" + + if explicitClose then false + else if explicitKeepAlive then true + else machine.config.enableKeepAlive && machine.reader.requestCount < machine.config.maxRequests + +@[inline] +private def updateKeepAlive (machine : Machine) : Machine := + { machine with keepAlive := determineKeepAlive machine } + +-- https://datatracker.ietf.org/doc/html/rfc7230#section-3.3.3 +def getRequestSize (req : Request.Head) : Option Body.Length := do + guard (req.headers.get? "host" |>.isSome) + + if req.method == .head ∨ req.method == .connect then + return .fixed 0 + + match (req.headers.get? "Content-Length", req.headers.hasEntry "Transfer-Encoding" "chunked") with + | (some cl, false) => do + let num ← cl.value.toNat? + some (.fixed num) + | (none, false) => + some (.fixed 0) + | (none, true) => + some .chunked + | (some _, true) => + some .chunked + +private def processHeaders (machine : Machine) : Machine := + let machine := updateKeepAlive machine + + match getRequestSize machine.reader.request with + | none => + machine.setFailure .badRequest .badRequest + | some size => + machine + |>.addEvent (.endHeaders machine.reader.request) + |>.setReaderState <| match size with + | .fixed n => .needFixedBody n + | .chunked => .needChunkedSize + +/-- +Set response headers and determine transfer mode +-/ +def setHeaders (response : Response.Head) (machine : Machine) : Machine := + let size := Writer.determineBodySize machine.writer + + let headers := + if let some server := machine.config.serverName then + response.headers + |>.insert "Server" server + else + response.headers + + let headers := + if let some date := machine.instant then + let date := date.format "EEE, dd MMM yyyy HH:mm:ss 'GMT'" + headers.insert "Date" (.ofString! date) + else + headers + + let headers := if ¬machine.keepAlive ∨ shouldBreakConnection response.status then + headers.insert "Connection" (.new "close") + else + headers + + let response := { response with headers } + + let response := match size with + | .fixed 0 => response + | .fixed n => { response with headers := response.headers.insert "Content-Length" (.ofString! <| toString n) } + | .chunked => { response with headers := response.headers.insert "Transfer-Encoding" (.new "chunked") } + + let state := match size with + | .fixed _ => Machine.Writer.State.writingFixedData + | .chunked => Machine.Writer.State.writingChunkedBody + + machine.modifyWriter (fun writer => { + writer with + outputData := writer.outputData.append (toString response).toUTF8, + state }) + +/-- +Remove all the events in the machine +-/ +@[inline] +def takeEvents (machine : Machine) : Machine × Array Event := + if machine.events.isEmpty then + (machine, machine.events) + else + ({ machine with events := #[] }, machine.events) + +/-- +Put some data inside the input of the machine. +-/ +@[inline] +def feed (machine : Machine) (data : ByteArray) : Machine := + { machine with reader := machine.reader.feed data } + +/-- +Put some data inside the input of the machine. +-/ +@[inline] +def setNow (machine : Machine) : IO Machine := do + return { machine with instant := some (← Std.Time.DateTime.now) } + +/-- +Put some data inside the input of the machine. +-/ +@[inline] +def writeUserData (machine : Machine) (data : Util.BufferBuilder) : Machine := + { machine with writer := machine.writer.addUserData data } + +/-- +Put some data inside the input of the machine. +-/ +@[inline] +def writeChunkExt (machine : Machine) (chunkExt : Array (String × Option String)) : Machine := + { machine with writer := machine.writer.addChunkExt chunkExt } + +/-- +Put some data inside the input of the machine. +-/ +@[inline] +def closeWriter (machine : Machine) : Machine := + { machine with writer := machine.writer.close } + +def isWriterOpened (machine : Machine) : Bool := + ¬machine.writer.closed + +def isWaitingResponse (machine : Machine) : Bool := + match machine.writer.state with + | .waitingHeaders => true + | _ => false + +/-- +Sends the response +-/ +def sendResponse (machine : Machine) (response : Response.Head) : Machine := + match machine.writer.state with + | .waitingHeaders => + let machine := machine.modifyWriter ({ · with response, state := .waitingForFlush }) + let conn := response.headers.getLast? "Connection" |>.getD (.new "Keep-Alive") + + if conn.is "close" then + machine + |>.closeConnection + |>.setReaderState .complete + else + machine + + | _ => + machine + +def isReaderComplete (machine : Machine) : Bool := + match machine.reader.state with + | .complete => true + | _ => false + +/-- +Advances the state of the reader. +-/ +partial def processRead (machine : Machine) : Machine := + match machine.reader.state with + | .needStartLine => + let (machine, result) := parseWith machine parseRequestLine (limit := some 8192) + + if let some head := result then + if head.version != .v11 then + machine + |>.setFailure .unsupportedVersion .badRequest + else + machine + |>.modifyReader (.setRequest head) + |>.setReaderState (.needHeader 0) + |>.processRead + else + machine + + | .needHeader headerCount => + let (machine, result) := parseWith machine (parseSingleHeader machine.config.maxHeaderSize) (limit := none) + + if headerCount > machine.config.maxHeaders then + machine |>.setFailure .badRequest .badRequest + else + if let some result := result then + if let some (name, value) := result then + if let some headerValue := HeaderValue.ofString? value then + machine + |>.modifyReader (.addHeader name headerValue) + |>.setReaderState (.needHeader (headerCount + 1)) + |>.processRead + else + machine.setFailure .badRequest .badRequest + else + processHeaders machine + else + machine + + | .requireResponse _ => + machine + + | .needChunkedSize => + let (machine, result) := parseWith machine parseChunkSize (limit := some 128) + + match result with + | some (size, ext) => + machine + |>.setReaderState (.needChunkedBody size) + |>.setEvent (some ext <&> .chunkExt) + |>.processRead + | none => + machine + + | .needChunkedBody size => + let (machine, result) := parseWith machine (parseChunkedSizedData size) (limit := none) (some size) + + if let some body := result then + match body with + | .complete body => + if size ≠ 0 then + machine + |>.setReaderState .needChunkedSize + |>.addEvent (.gotData false body) + |>.processRead + else + machine + |>.setReaderState .complete + |>.addEvent (.gotData true .empty) + |>.processRead + | .incomplete body remaining => machine + |>.setReaderState (.needChunkedBody remaining) + |>.addEvent (.gotData false body) + else + machine + + | .needFixedBody 0 => + machine + |>.setReaderState .complete + |>.addEvent (.gotData true .empty) + |>.processRead + + | .needFixedBody size => + let (machine, result) := parseWith machine (parseFixedSizeData size) (limit := none) (some size) + + if let some body := result then + match body with + | .complete body => + machine + |>.setReaderState .complete + |>.addEvent (.gotData true body) + |>.processRead + | .incomplete body remaining => + machine + |>.setReaderState (.needFixedBody remaining) + |>.addEvent (.gotData false body) + else + machine + + | .complete => + machine + + | .failed response => + machine + |>.sendResponse response + |>.resetAndClose + |>.setReaderState .complete + |>.closeConnection + +def failed (machine : Machine) : Bool := + match machine.reader.state with + | .failed _ => true + | _ => false + +def shouldFlush (machine : Machine) : Bool := + machine.failed ∨ + machine.writer.userData.size ≥ machine.config.highMark ∨ + machine.writer.closed + +/-- +Get the current output data and clear the buffer +-/ +@[inline] +def takeOutput (machine : Machine) (highMark := 0) : Option (Machine × BufferBuilder) := + if machine.writer.outputData.size ≥ highMark ∨ + machine.writer.state == .complete + then + let output := machine.writer.outputData + some ({ machine with writer := { machine.writer with outputData := .empty } }, output) + else + none + +/-- +Write response data to the machine +-/ +partial def processWrite (machine : Machine) : Machine := + match machine.writer.state with + | .waitingHeaders => + machine + + | .waitingForFlush => + if machine.shouldFlush then + machine.setHeaders machine.writer.response |>.processWrite + else + machine + + | .writingFixedData => + if machine.writer.userData.size ≥ machine.config.highMark ∨ machine.writer.closed then + let machine := machine.modifyWriter Writer.writeFixedBody + if machine.writer.closed then + machine.setWriterState .complete |>.processWrite + else + machine + else + machine + + | .writingChunkedBody => + if machine.writer.closed then + machine.modifyWriter Writer.writeFinalChunk |>.processWrite + else if machine.writer.userData.size ≥ machine.config.highMark then + machine.modifyWriter Writer.writeChunkedBody |>.processWrite + else + machine + + | .complete => + resetForNextRequest machine + + | .writingHeaders => + machine + +end Machine diff --git a/src/Std/Internal/Http/Protocol/H1/Parser.lean b/src/Std/Internal/Http/Protocol/H1/Parser.lean new file mode 100644 index 000000000000..9db4e1ee3333 --- /dev/null +++ b/src/Std/Internal/Http/Protocol/H1/Parser.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Parsec +public import Std.Internal.Http.Data +public import Std.Internal.Parsec.ByteArray + +namespace Std +namespace Http +namespace Protocol +namespace H1 + +open Std Internal Parsec ByteArray Util + +/-! +This module defines a parser for HTTP/1.1 requests. The reference used is https://httpwg.org/specs/rfc9112.html. +-/ + +set_option linter.all true + +@[inline] +def isDigit (c : UInt8) : Bool := + c ≥ '0'.toUInt8 ∧ c ≤ '9'.toUInt8 + +@[inline] +def isAlpha (c : UInt8) : Bool := + (c ≥ 'a'.toUInt8 ∧ c ≤ 'z'.toUInt8) ∨ (c ≥ 'A'.toUInt8 ∧ c ≤ 'Z'.toUInt8) + +@[inline] +def isVChar (c : UInt8) : Bool := + c ≥ 0x21 ∧ c ≤ 128 + +def isTokenCharacter (c : UInt8) : Bool := + isDigit c ∨ isAlpha c ∨ c == '!'.toUInt8 ∨ c == '#'.toUInt8 ∨ c == '$'.toUInt8 ∨ c == '%'.toUInt8 ∨ + c == '&'.toUInt8 ∨ c == '\''.toUInt8 ∨ c == '*'.toUInt8 ∨ c == '+'.toUInt8 ∨ c == '-'.toUInt8 ∨ + c == '.'.toUInt8 ∨ c == '^'.toUInt8 ∨ c == '_'.toUInt8 ∨ c == '`'.toUInt8 ∨ c == '|'.toUInt8 ∨ + c == '~'.toUInt8 + +@[inline] +def isObsChar (c : UInt8) : Bool := + c ≥ 0x80 ∧ c ≤ 0xFF + +@[inline] +def isFieldVChar (c : UInt8) : Bool := + isVChar c ∨ isObsChar c ∨ c = ' '.toUInt8 ∨ c = '\t'.toUInt8 + + +-- HTAB / SP / %x21 / %x23-5B / %x5D-7E / obs-text +@[inline] +def isQdText (c : UInt8) : Bool := + c == '\t'.toUInt8 ∨ + c == ' '.toUInt8 ∨ + c == '!'.toUInt8 ∨ + (c ≥ '#'.toUInt8 ∧ c ≤ '['.toUInt8) ∨ + (c ≥ ']'.toUInt8 ∧ c ≤ '~'.toUInt8) ∨ + isObsChar c + +-- Parser blocks + +def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) : Parser (Array α) := do + let items ← many (attempt <| parser.bind (fun item => match item with + | some x => return x + | none => fail "end of items")) + if items.size > maxCount then + fail s!"Too many items: {items.size} > {maxCount}" + return items + +def opt (x : Option α) : Parser α := + if let some res := x then + return res + else + fail "expected value but got none" + +@[inline] +def token (limit : Nat) : Parser ByteSlice := + takeWhileUpTo1 isTokenCharacter limit + +@[inline] +def crlf : Parser Unit := + skipBytes "\r\n".toUTF8 + +@[inline] +def rsp : Parser Unit := + discard <| takeWhileUpTo1 (· == ' '.toUInt8) 256 + +@[inline] +def osp : Parser Unit := + discard <| takeWhileUpTo (· == ' '.toUInt8) 256 + +@[inline] +def uint8 : Parser UInt8 := do + let d ← digit + return d.toUInt8 + +def hexDigit : Parser UInt8 := do + let b ← any + if b ≥ '0'.toUInt8 && b ≤ '9'.toUInt8 then return b - '0'.toUInt8 + else if b ≥ 'A'.toUInt8 && b ≤ 'F'.toUInt8 then return b - 'A'.toUInt8 + 10 + else if b ≥ 'a'.toUInt8 && b ≤ 'f'.toUInt8 then return b - 'a'.toUInt8 + 10 + else fail s!"Invalid hex digit {Char.ofUInt8 b |>.quote}" + +@[inline] +def hex : Parser Nat := do + let hexDigits ← many1 (attempt hexDigit) + return (hexDigits.foldl (fun acc cur => acc * 16 + cur.toNat) 0) + +-- Actual parsers + +-- HTTP-version = HTTP-name "/" DIGIT "." DIGIT +-- HTTP-name = %s"HTTP" +def parseHttpVersion : Parser Version := do + skipBytes "HTTP/".toUTF8 + let major ← uint8 + skipByte '.'.toUInt8 + let minor ← uint8 + opt <| Version.fromNumber? (major - 48 |>.toNat) (minor - 48 |>.toNat) + +-- method = token +def parseMethod : Parser Method := do + let method ← token 16 + opt <| Method.fromString? (String.fromUTF8! method.toByteArray) + +def parseURI : Parser String := do + let uri ← takeUntil (· == ' '.toUInt8) + return String.fromUTF8! uri.toByteArray + +/-- +Parses a request line + +request-line = method SP request-target SP HTTP-version +-/ +public def parseRequestLine : Parser Request.Head := do + let method ← parseMethod <* rsp + let uri ← Std.Http.Parser.parseRequestTarget <* rsp + let version ← parseHttpVersion <* crlf + return ⟨method, version, uri, .empty⟩ + +-- field-line = field-name ":" OWS field-value OWS +def parseFieldLine (headerLimit : Nat) : Parser (String × String) := do + (String.fromUTF8! ·.toByteArray, String.fromUTF8! ·.toByteArray) <$> + token 256 <*> (skipByte ':'.toUInt8 *> osp *> takeWhileUpTo1 isFieldVChar headerLimit <* osp) + +/-- +Parses a single header. + +field-line CRLF / CRLF +-/ +public def parseSingleHeader (headerLimit : Nat) : Parser (Option (String × String)) := + optional (attempt <| parseFieldLine headerLimit) <* crlf + +-- quoted-pair = "\" ( HTAB / SP / VCHAR / obs-text ) +def parseQuotedPair : Parser UInt8 := do + skipByte '\\'.toUInt8 + let b ← any + + if b == '\t'.toUInt8 ∨ b == ' '.toUInt8 || isVChar b || isObsChar b then + return b + else + fail s!"invalid quoted-pair byte: {Char.ofUInt8 b |>.quote}" + +-- quoted-string = DQUOTE *( qdtext / quoted-pair ) DQUOTE +partial def parseQuotedString : Parser String := do + skipByte '"'.toUInt8 + + let rec loop (buf : ByteArray) : Parser ByteArray := do + let b ← any + + if b == '"'.toUInt8 then + return buf + else if b == '\\'.toUInt8 then + let next ← any + if next == '\t'.toUInt8 ∨ next == ' '.toUInt8 ∨ isVChar next ∨ isObsChar next + then loop (buf.push next) + else fail s!"invalid quoted-pair byte: {Char.ofUInt8 next |>.quote}" + else if isQdText b then + loop (buf.push b) + else + fail s!"invalid qdtext byte: {Char.ofUInt8 b |>.quote}" + + return String.fromUTF8! (← loop .empty) + +-- chunk-ext = *( BWS ";" BWS chunk-ext-name [ BWS "=" BWS chunk-ext-val] ) +def parseChunkExt : Parser (String × Option String) := do + osp *> skipByte ';'.toUInt8 *> osp + let name ← (String.fromUTF8! <$> ByteSlice.toByteArray <$> token 256) <* osp + + if (← peekWhen? (· == '='.toUInt8)) |>.isSome then + osp *> skipByte '='.toUInt8 *> osp + let value ← osp *> (parseQuotedString <|> String.fromUTF8! <$> ByteSlice.toByteArray <$> token 256) + return (name, some value) + + return (name, none) + +/-- +This function parses the size and extension of a chunk +-/ +public def parseChunkSize : Parser (Nat × Array (String × Option String)) := do + let size ← hex + let ext ← many parseChunkExt + crlf + return (size, ext) + +/-- +Result of parsing partial or complete information. +-/ +public inductive TakeResult + | complete (data : ByteSlice) + | incomplete (data : ByteSlice) (remaining : Nat) + +/-- +Parses a fixed size data that can be incomplete. +-/ +public def parseFixedSizeData (size : Nat) : Parser TakeResult := fun it => + if it.remainingBytes = 0 then + .error it .eof + else if it.remainingBytes < size then + .success (it.forward it.remainingBytes) (.incomplete it.array[it.idx...(it.idx+it.remainingBytes)] (size - it.remainingBytes)) + else + .success (it.forward size) (.complete (it.array[it.idx...(it.idx+size)])) + +/-- +Parses a fixed size data that can be incomplete. +-/ +public def parseChunkedSizedData (size : Nat) : Parser TakeResult := do + match ← parseFixedSizeData size with + | .complete data => crlf *> return .complete data + | .incomplete data res => return .incomplete data res + +/-- +This function parses a single chunk in chunked transfer encoding +-/ +public def parseChunk : Parser (Option (Nat × Array (String × Option String) × ByteSlice)) := do + let (size, ext) ← parseChunkSize + if size == 0 then + return none + else + let data ← take size + return some ⟨size, ext, data⟩ +/-- +This function parses a trailer header (used after chunked body) +-/ +def parseTrailerHeader (headerLimit : Nat) : Parser (Option (String × String)) := parseSingleHeader headerLimit + +/-- +This function parses trailer headers after chunked body +-/ +public def parseTrailers (headerLimit : Nat) : Parser (Array (String × String)) := do + let trailers ← manyItems (parseTrailerHeader headerLimit) 100 + crlf + return trailers + +end H1 +end Protocol +end Http +end Std diff --git a/src/Std/Internal/Http/Server.lean b/src/Std/Internal/Http/Server.lean new file mode 100644 index 000000000000..bb3a8ad4070a --- /dev/null +++ b/src/Std/Internal/Http/Server.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Server.Connection +public import Std.Internal.Http.Server.ClientConnection + +public section + +namespace Std +namespace Http +namespace Server + +open Std Internal IO Async TCP +open Time + +/-- +Serve conection +-/ +def serve + (addr : Net.SocketAddress) + (onRequest : Request Body → Async (Response Body)) + (config : Config := {}) (backlog : UInt32 := 128) : Async Unit := do + let server ← Socket.Server.mk + server.bind addr + server.listen backlog + + while true do + let client ← server.accept + background (prio := .max) <| serveConnection client onRequest config diff --git a/src/Std/Internal/Http/Server/ClientConnection.lean b/src/Std/Internal/Http/Server/ClientConnection.lean new file mode 100644 index 000000000000..26cd0f088f3b --- /dev/null +++ b/src/Std/Internal/Http/Server/ClientConnection.lean @@ -0,0 +1,267 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Protocol.H1 + +public section + +namespace Std +namespace Http +namespace Server + +open Std Internal IO Async TCP + +/-- +Generic HTTP client interface that abstracts over different transport mechanisms. +-/ +class ClientConnection (α : Type) where + /-- + Receive data from the client connection, up to the expected size. + Returns None if the connection is closed or no data is available. + -/ + recv : α → UInt64 → Async (Option ByteArray) + + /-- + Send all data through the client connection. + -/ + sendAll : α → Array ByteArray → Async Unit + + /-- + Get a selector for receiving data asynchronously. + -/ + recvSelector : α → UInt64 → Async (Selector (Option ByteArray)) + +instance : ClientConnection Socket.Client where + recv client expect := client.recv? expect + sendAll client data := client.sendAll data + recvSelector client expect := client.recvSelector expect + +open Internal.IO.Async in +inductive MockClient.Consumer where + | normal (promise : IO.Promise (Option ByteArray)) + | select (waiter : Waiter (Option ByteArray)) + +def MockClient.Consumer.resolve (c : MockClient.Consumer) (data : Option ByteArray) : BaseIO Bool := do + match c with + | .normal promise => + promise.resolve data + return true + | .select waiter => + let lose := return false + let win promise := do + promise.resolve (.ok data) + return true + waiter.race lose win + +structure MockClient.State where + /-- + Queue of data to be received by the client. + -/ + receiveQueue : ByteArray := .empty + + /-- + Consumers that are blocked waiting for data. + -/ + consumers : Std.Queue MockClient.Consumer := .empty + + /-- + Buffer containing all data sent through this client. + -/ + sentData : ByteArray := .empty + + /-- + Flag indicating whether the connection is closed. + -/ + closed : Bool := false + +/-- +Mock client socket for testing HTTP interactions. +-/ +structure Mock.Client where + /-- + State + -/ + state : Std.Mutex MockClient.State + +namespace Mock.Client + +/-- +Create a new mock client with empty buffers. +-/ +def new : BaseIO Mock.Client := do + let state ← Std.Mutex.new { + receiveQueue := .empty, + consumers := .empty, + sentData := .empty, + closed := false + } + return { state } + +/-- +Add data to the receive queue for testing and notify any waiting receivers. +-/ +def enqueueReceive (client : Mock.Client) (data : ByteArray) : BaseIO Unit := do + client.state.atomically do + let st ← get + if st.closed then + return () + + let mut newQueue := st.receiveQueue ++ data + set { st with receiveQueue := newQueue } + + while true do + let st ← get + if let some (consumer, consumers) := st.consumers.dequeue? then + if st.receiveQueue.size > 0 then + discard <| consumer.resolve (some st.receiveQueue) + set { st with + receiveQueue := .empty, + consumers + } + else + break + else + break + +/-- +Close the mock connection and notify all waiters. +-/ +def close (client : Mock.Client) : BaseIO Unit := do + client.state.atomically do + let st ← get + for consumer in st.consumers.toArray do + discard <| consumer.resolve none + + set { st with + closed := true, + consumers := .empty + } + +/-- +Get all data that was sent through this client. +-/ +def getSentData (client : Mock.Client) : BaseIO ByteArray := + client.state.atomically do + let st ← get + return st.sentData + +/-- +Clear the sent data buffer. +-/ +def clearSentData (client : Mock.Client) : BaseIO Unit := + client.state.atomically do + modify fun st => { st with sentData := .empty } + +/-- +Check if the connection is closed. +-/ +def isClosed (client : Mock.Client) : BaseIO Bool := + client.state.atomically do + let st ← get + return st.closed + +/-- +Try to receive data immediately without blocking. +-/ +private def tryRecv' (size : UInt64) : AtomicT MockClient.State Async (Option ByteArray) := do + let st ← get + if st.closed then + return none + + if st.receiveQueue.isEmpty then + return none + else + let data := st.receiveQueue + let requested := data.extract 0 size.toNat + let remainder := data.extract size.toNat data.size + set { st with receiveQueue := remainder } + return some requested + +/-- +Try to receive data immediately without blocking. +-/ +def tryRecv (client : Mock.Client) (size : UInt64) : Async (Option ByteArray) := + client.state.atomically do + tryRecv' size + +/-- +Check if data is ready to be received. +-/ +@[inline] +private def recvReady' : AtomicT MockClient.State Async Bool := do + let st ← get + return !st.receiveQueue.isEmpty || st.closed + +/-- +Receive data from the mock client, simulating network behavior. +-/ +def recv? (client : Mock.Client) (size : UInt64) : Async (Option ByteArray) := do + client.state.atomically do + if let some data ← tryRecv' size then + return (some data) + else if (← get).closed then + return none + else + let promise ← IO.Promise.new + modify fun st => { st with consumers := st.consumers.enqueue (.normal promise) } + Async.ofTask promise.result! + +/-- +Send all data through the mock client by appending to the sent data buffer. +-/ +def sendAll (client : Mock.Client) (data : Array ByteArray) : Async Unit := do + let closed ← client.state.atomically do + let st ← get + if st.closed then + return true + else + let combinedData := data.foldl ByteArray.append .empty + set { st with sentData := st.sentData ++ combinedData } + + return false + + if closed then + throw (.userError "Cannot send on closed connection") + +/-- +Create a selector for receiving data asynchronously. +-/ +def recvSelector (client : Mock.Client) (size : UInt64) : Async (Selector (Option ByteArray)) := do + return { + tryFn := do + client.state.atomically do + if ← recvReady' then + let data ← tryRecv' size + return some data + else + return none + + registerFn := fun waiter => do + let lose := return () + let win promise := do + promise.resolve (.ok none) + waiter.race lose win + + unregisterFn := do + client.state.atomically do + let st ← get + let consumers ← st.consumers.filterM fun + | .normal _ => return true + | .select waiter => return !(← waiter.checkFinished) + set { st with consumers } + } + +instance : ClientConnection Mock.Client where + recv := Mock.Client.recv? + sendAll := Mock.Client.sendAll + recvSelector := Mock.Client.recvSelector + +end Mock.Client +end Server +end Http +end Std diff --git a/src/Std/Internal/Http/Server/Config.lean b/src/Std/Internal/Http/Server/Config.lean new file mode 100644 index 000000000000..01eda941b4e6 --- /dev/null +++ b/src/Std/Internal/Http/Server/Config.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Time +public import Std.Internal.Http.Protocol.H1 + +public section + +namespace Std +namespace Http + +/-- +Connection limits configuration with validation. +-/ +structure Config where + /-- + Maximum number of requests per connection. + -/ + maxRequests : Nat := 100 + + /-- + Maximum number of headers allowed per request. + -/ + maxHeaders : Nat := 50 + + /-- + Maximum size of a single header value. + -/ + maxHeaderSize : Nat := 8192 + + /-- + Maximum waiting time for more data. + -/ + lingeringTimeout : Time.Millisecond.Offset := 5000 + + /-- + Timeout for keep-alive connections + -/ + keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨45000, by decide⟩ + + /-- + Maximum timeout time for request more data. + -/ + requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨10000, by decide⟩ + + /-- + Whether to enable keep-alive connections by default. + -/ + enableKeepAlive : Bool := true + + /-- + Size threshold for flushing output buffer. + -/ + highMark : Nat := 4096 + + /-- + The maximum size that the connection can receive in a single recv call. + -/ + maximumRecvSize : Nat := 8192 + + /-- + Default buffer size for the connection + -/ + defaultPayloadBytes : Nat := 8192 + + /-- + The server name. + -/ + serverName : Option HeaderValue := some (.new "LeanHTTP/1.1") + +namespace Config + +/-- +Converts to HTTP 1.1 config +-/ +def toH1Config (config : Config) : Protocol.H1.Machine.Config := + { maxRequests := config.maxRequests + maxHeaders := config.maxHeaders + maxHeaderSize := config.maxHeaderSize + enableKeepAlive := config.enableKeepAlive + highMark := config.highMark + serverName := config.serverName + } diff --git a/src/Std/Internal/Http/Server/Connection.lean b/src/Std/Internal/Http/Server/Connection.lean new file mode 100644 index 000000000000..8a394460f26a --- /dev/null +++ b/src/Std/Internal/Http/Server/Connection.lean @@ -0,0 +1,246 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Async.TCP +public import Std.Internal.Http.Protocol.H1 +public import Std.Internal.Http.Server.Config +public import Std.Internal.Http.Server.ClientConnection + +public section + +namespace Std +namespace Http +namespace Server + +open Std Internal IO Async TCP +open Time + +/-! +This module defines a `Server.Connection` that is a structure used to handle a single HTTP connection with +possibly multiple requests. +-/ + +set_option linter.all true + +/-- +A single HTTP connection. +-/ +public structure Connection (α : Type) where + /-- + The client connection. + -/ + socket : α + + /-- + The processing machine for HTTP 1.1 + -/ + machine : Protocol.H1.Machine + +namespace Connection + +private inductive Recv + | bytes (x : Option ByteArray) + | timeout + +private def receiveWithTimeout [ClientConnection α] (socket : α) (expect : UInt64) + (timeoutMs : Millisecond.Offset) : + Async Recv := do + Selectable.one #[ + .case (← ClientConnection.recvSelector socket expect) (fun x => pure <| .bytes x), + .case (← Selector.sleep timeoutMs) (fun _ => pure <| .timeout)] + +private def processNeedMoreData + [ClientConnection α] (config : Config) (socket : α) (expect : Option Nat) : + Async (Except Protocol.H1.Machine.Error (Option ByteArray)) := do + try + let expect := expect + |>.getD config.defaultPayloadBytes + |>.min config.maximumRecvSize + + let data ← receiveWithTimeout socket expect.toUInt64 config.lingeringTimeout + + match data with + | .bytes (some bytes) => pure (.ok <| some bytes) + | .bytes none => pure (.ok <| none) + | .timeout => pure (.error Protocol.H1.Machine.Error.timeout) + + catch _ => + pure (.error Protocol.H1.Machine.Error.timeout) + +private def handle + [ClientConnection α] + (connection : Connection α) + (config : Config) + (handler : Request Body → Async (Response Body)) : Async Unit := do + + let mut machine := connection.machine + let mut running := true + let socket := connection.socket + + let mut requestStream ← Body.ByteStream.emptyWithCapacity + let mut requestTimer ← Interval.mk config.requestTimeout.val config.requestTimeout.property + let mut connectionTimer ← Sleep.mk config.keepAliveTimeout + + let mut response ← IO.Promise.new + let mut errored ← IO.Promise.new + let mut respStream := none + let mut sentResponse := false + let mut closing := false + + -- Wait for the first tick that is immediate + requestTimer.tick + + let mut requestTimerTask ← async requestTimer.tick + let connectionTimerTask ← async connectionTimer.wait + + while running do + machine := machine.processRead.processWrite + + let (newMachine, events) := machine.takeEvents + machine := newMachine + + -- Process events like receiving data from the socket. + for event in events do + match event with + | .needMoreData expect => do + try + match ← processNeedMoreData config socket expect with + | .ok (some bs) => + machine := machine.feed bs + | .ok none => + running := false; + break + | .error _ => do + if let .needStartLine := machine.reader.state then + running := false; break + else + machine := machine.setFailure .timeout .requestTimeout + catch _ => + running := false + + | .endHeaders head => do + if let some (.fixed n) := Protocol.H1.Machine.getRequestSize head then + requestStream.setKnownSize (some n) + + let newResponse := handler { head, body := (.stream requestStream) } + let task ← newResponse.asTask + + BaseIO.chainTask task fun + | .error res => errored.resolve res + | .ok res => response.resolve res + + | .gotData final data => + discard <| requestStream.send data.toByteArray + + if final then + requestStream.close + + | .chunkExt _ => + pure () + + | .failed => + pure () + + | .close => + running := false + + | .next => + requestTimer.reset + requestStream ← Body.ByteStream.emptyWithCapacity + response ← IO.Promise.new + errored ← IO.Promise.new + respStream := none + sentResponse := false + + -- Sends the response head and starts to receive the response body. + if not sentResponse ∧ (← response.isResolved) then + sentResponse := true + let res ← await response.result! + + if machine.isWaitingResponse then + machine := machine.sendResponse res.head + match res.body with + | some (.bytes data) => machine := machine.writeUserData data |>.closeWriter + | some ( .zero) | none => machine := machine.closeWriter + | some (.stream res) => do + if let some size ← res.getKnownSize then + machine := machine.setKnownSize size + + respStream := some res + + -- Sends data from the response body. + if let some stream := respStream then + if machine.isWriterOpened then + if machine.isReaderComplete ∧ events.isEmpty then + if let some data ← stream.recv then + machine := machine.writeUserData data + else + machine := machine.closeWriter + else + if ← stream.isClosed then + pure () + else + match ← stream.tryRecv with + | some res => machine := machine.writeUserData res + | none => machine := machine.closeWriter + + -- Checks for things that can close the connection. + if ¬closing then + if (← requestTimerTask.isFinished) ∨ (← connectionTimerTask.isFinished) then + machine := machine.setFailure .timeout .requestTimeout + closing := true + + if ← errored.isResolved then + let _ ← await errored.result! + machine := machine.setFailure (.other "Internal Error") .internalServerError + closing := true + + -- Sends the output of the machine to the socket in a vectored write. + if let some (newMachine, data) := machine.takeOutput then + machine := newMachine + + if data.size > 0 then + try + ClientConnection.sendAll socket data.data + catch _ => + running := false + + -- End of the connection + connectionTimer.stop + requestTimer.stop + +end Connection + +/-- +This is the entry point of the library. It is used to receive and send requests using an `Async` +handler for a single connection. It can be used with a `TCP.Socket` or any other type that implements +`ClientConnection` to create a simple HTTP server capable of handling multiple connections concurrently. + +# Example + +```lean +-- Create a TCP socket server instance +let server ← Socket.Server.mk +server.bind addr +server.listen backlog + +-- Enter an infinite loop to handle incoming client connections +while true do + -- Accept a new client connection. + let client ← server.accept + + -- Handle the client connection concurrently in the background `serveConnection` will process requests + -- and handle failures using the provided callbacks and config + background (serveConnection client onRequest onFailure config) +``` + +-/ +def serveConnection [ClientConnection t] (client : t) + (onRequest : Request Body → Async (Response Body)) (config : Config := {}) : Async Unit := do + Connection.mk client { config := config.toH1Config } + |>.handle config onRequest diff --git a/src/Std/Internal/Http/Util.lean b/src/Std/Internal/Http/Util.lean new file mode 100644 index 000000000000..d1ed0b63fc37 --- /dev/null +++ b/src/Std/Internal/Http/Util.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Internal.Http.Util.Buffer +public import Std.Internal.Http.Util.BufferBuilder diff --git a/src/Std/Internal/Http/Util/Buffer.lean b/src/Std/Internal/Http/Util/Buffer.lean new file mode 100644 index 000000000000..3c9e5ee21215 --- /dev/null +++ b/src/Std/Internal/Http/Util/Buffer.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.String +public import Init.Data.ByteArray + +public section + +namespace Std +namespace Http +namespace Util + +set_option linter.all true + +/-- +A `Buffer` is a type alias for `ByteArray` that provides a convenient interface for working with binary data. +-/ +@[expose] +def Buffer := ByteArray + +namespace Buffer + +/-- +Creates a buffer with minimum size of `1024` if not specified. +-/ +@[inline] +def empty (capacity := 1024) : Buffer := + ByteArray.emptyWithCapacity capacity + +/-- +Writes a `ByteArray` to the `Buffer` +-/ +@[inline] +def write (buffer : Buffer) (data : ByteArray) : Buffer := + buffer.append data + +/-- +Writes a `Char` to the `Buffer` +-/ +@[inline] +def writeChar (buffer : Buffer) (data : Char) : Buffer := + buffer.push data.toUInt8 + +/-- +Writes a `String` to the `Buffer` +-/ +@[inline] +def writeString (buffer : Buffer) (data : String) : Buffer := + buffer.append data.toUTF8 diff --git a/src/Std/Internal/Http/Util/BufferBuilder.lean b/src/Std/Internal/Http/Util/BufferBuilder.lean new file mode 100644 index 000000000000..2c2d44ace978 --- /dev/null +++ b/src/Std/Internal/Http/Util/BufferBuilder.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.Data.ByteArray + +public section + +namespace Std +namespace Http +namespace Util + +/- +A structure that holds a bunch of ByteArrays and tracks the total size. +-/ +structure BufferBuilder where + data : Array ByteArray + size : Nat +deriving Inhabited + +namespace BufferBuilder + +/-- +An empty byte builder. +-/ +@[inline] +def empty : BufferBuilder := + { data := #[], size := 0 } + +/-- +Append a single ByteArray to the byte builder. +-/ +@[inline] +def push (c : BufferBuilder) (b : ByteArray) : BufferBuilder := + { data := c.data.push b, size := c.size + b.size } + +/-- +Append many ByteArrays at once. +-/ +@[inline] +def append (c : BufferBuilder) (d : BufferBuilder) : BufferBuilder := + { data := c.data ++ d.data, size := c.size + d.size } + +/-- +Turn the combined structure into a single contiguous ByteArray. +-/ +@[inline] +def toByteArray (c : BufferBuilder) : ByteArray := + if h : 1 = c.data.size then + c.data[0]'(Nat.le_of_eq h) + else + c.data.foldl (· ++ ·) (.emptyWithCapacity c.size) + +/-- +Build from a ByteArray directly. +-/ +@[inline] +def ofByteArray (bs : ByteArray) : BufferBuilder := + { data := #[bs], size := bs.size } + +/-- +Build from an array of ByteArrays directly. +-/ +@[inline] +def fromArray (bs : Array ByteArray) : BufferBuilder := + { data := bs, size := bs.foldl (· + ·.size) 0 } + +/-- +Check if it's an empty array. +-/ +@[inline] +def isEmpty (bb : BufferBuilder) : Bool := + bb.size = 0 + +instance : HAppend BufferBuilder BufferBuilder BufferBuilder where + hAppend := append + +instance : Coe ByteArray BufferBuilder where + coe := ofByteArray + +instance : Coe (Array ByteArray) BufferBuilder where + coe := fromArray + +end BufferBuilder +end Util +end Http +end Std diff --git a/tests/lean/run/async_http_parser.lean b/tests/lean/run/async_http_parser.lean new file mode 100644 index 000000000000..c290713f974b --- /dev/null +++ b/tests/lean/run/async_http_parser.lean @@ -0,0 +1,207 @@ +import Std.Internal.Http.Protocol.H1.Parser + +open Std.Http.Protocol + +def runParser (parser : Std.Internal.Parsec.ByteArray.Parser α) (s : String) : IO α := + IO.ofExcept (parser.run s.toUTF8) + +-- Chunk parsing tests +/-- +info: 16 / #[] / "adasdssdabcdabde" +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser H1.parseChunk "10\r\nadasdssdabcdabde" + match result with + | some (size, ext, body) => IO.println s!"{size} / {ext} / {String.fromUTF8! body.toByteArray |>.quote}" + | none => IO.println "end chunk" + +/-- +info: end chunk +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser H1.parseChunk "0\r\n" + match result with + | some (size, ext, body) => IO.println s!"{size} / {ext} / {String.fromUTF8! body.toByteArray |>.quote}" + | none => IO.println "end chunk" + +/-- +info: 255 / #[] / "This is a test chunk with exactly 255 bytes of data. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris lorem ipsu." +-/ +#guard_msgs in +#eval show IO _ from do + let testData := "This is a test chunk with exactly 255 bytes of data. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris lorem ipsu." + let result ← runParser H1.parseChunk s!"FF\r\n{testData}" + match result with + | some (size, ext, body) => IO.println s!"{size} / {ext} / {String.fromUTF8! body.toByteArray |>.quote}" + | none => IO.println "end chunk" + +-- Chunk size parsing tests (refactored to use runParser) +/-- +info: 16 / #[(abc, none), (def, none), (g, (some h))] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseChunkSize "10;abc;def;g=h\r\n" + IO.println s!"{result.1} / {result.2}" + +/-- +info: 0 / #[(abc, none), (def, none), (g, (some h))] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseChunkSize "0;abc;def;g=h\r\n" + IO.println s!"{result.1} / {result.2}" + +/-- +info: 4095 / #[] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseChunkSize "FFF\r\n" + IO.println s!"{result.1} / {result.2}" + +/-- +info: 1 / #[(name, (some (value with spaces)))] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseChunkSize "1;name=\"value with spaces\"\r\n" + IO.println s!"{result.1} / {result.2}" + +-- Single header parsing tests (refactored to use runParser) +/-- +info: User-Agent / "Mozilla/5.0 (X11; Linux x86_64; rv:143.0) Gecko/20100101 Firefox/143.0" +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseSingleHeader 256) "User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:143.0) Gecko/20100101 Firefox/143.0\r\n" + match result with + | some (k, v) => IO.println s!"{k} / {v.quote}" + | none => IO.println "end" + +/-- +info: Content-Type / "application/json; charset=utf-8" +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseSingleHeader 256) "Content-Type: application/json; charset=utf-8\r\n" + match result with + | some (k, v) => IO.println s!"{k} / {v.quote}" + | none => IO.println "end" + +/-- +info: Authorization / Bearer eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseSingleHeader 256) "Authorization: Bearer eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9\r\n" + match result with + | some (k, v) => IO.println s!"{k} / {v}" + | none => IO.println "end" + +/-- +info: end +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseSingleHeader 256) "\r\n" + match result with + | some (k, v) => IO.println s!"{k} / {v}" + | none => IO.println "end" + +/-- +error: offset 0: unexpected end of input +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseTrailers 256) "" + IO.println s!"{result}" + +/-- +info: #[] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseTrailers 256) "\r\n" + IO.println s!"{result}" + +/-- +info: #[(X-Checksum, abc123), (X-Timestamp, 2023-01-01T12:00:00Z)] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseTrailers 256) "X-Checksum: abc123\r\nX-Timestamp: 2023-01-01T12:00:00Z\r\n\r\n" + IO.println s!"{result}" + +-- Request line parsing tests (refactored to use runParser) +/-- +info: Std.Http.Method.get / Std.Http.RequestTarget.originForm { segments := #["ata", ""], absolute := true } none none / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "GET /ata/ HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +/-- +info: Std.Http.Method.post / Std.Http.RequestTarget.originForm { segments := #["api", "v1", "users"], absolute := true } none none / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "POST /api/v1/users HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +/-- +info: Std.Http.Method.put / Std.Http.RequestTarget.originForm + { segments := #["data"], absolute := true } + (some #[("param1", some "value1"), ("param2", some "value2")]) + none / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "PUT /data?param1=value1¶m2=value2 HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +/-- +info: Std.Http.Method.delete / Std.Http.RequestTarget.originForm { segments := #["items", "123"], absolute := true } none none / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "DELETE /items/123 HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +/-- +info: Std.Http.Method.head / Std.Http.RequestTarget.originForm { segments := #[""], absolute := true } none none / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "HEAD / HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +/-- +info: Std.Http.Method.options / Std.Http.RequestTarget.asteriskForm / Std.Http.Version.v11 +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseRequestLine "OPTIONS * HTTP/1.1\r\n" + IO.println s!"{repr result.method} / {repr result.uri} / {repr result.version}" + +-- Additional edge case tests +/-- +info: 0 / #[] +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Protocol.H1.parseChunkSize "0\r\n" + IO.println s!"{result.1} / {result.2}" + +/-- +info: X-Custom-Header / value with multiple spaces +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser (Std.Http.Protocol.H1.parseSingleHeader 256) "X-Custom-Header: value with multiple spaces\r\n" + match result with + | some (k, v) => IO.println s!"{k} / {v}" + | none => IO.println "end" diff --git a/tests/lean/run/async_http_uri_parser.lean b/tests/lean/run/async_http_uri_parser.lean new file mode 100644 index 000000000000..767d8cae102e --- /dev/null +++ b/tests/lean/run/async_http_uri_parser.lean @@ -0,0 +1,335 @@ +import Std.Internal.Http.Protocol.H1.Parser + +open Std.Http.Protocol + +def runParser (parser : Std.Internal.Parsec.ByteArray.Parser α) (s : String) : IO α := + IO.ofExcept (parser.run s.toUTF8) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #["path", "with", "encoded space"], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/path/with/encoded%20space" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #["path", "with", "encoded space", ""], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/path/with/encoded%20space/" + IO.println (repr result) + +/-- +error: offset 0: invalid request target +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "path/with/encoded%20space" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.asteriskForm +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "*" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "ata", port := none }, + path := { segments := #["b"], absolute := true }, + query := some #[("ata", some "be")], + fragment := some "lol🔥" } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://ata/b?ata=be#lol%F0%9F%94%A5" + IO.println (repr result) +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["api", "search"], absolute := true } + (some #[("q", some "hello world"), ("category", some "tech+games")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/api/search?q=hello%20world&category=tech%2Bgames" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #["files", "my document.pdf"], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/files/my%20document%2Epdf" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["search"], absolute := true } + (some #[("name", some "✓ checked"), ("emoji", some "😀")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/search?name=%E2%9C%93%20checked&emoji=%F0%9F%98%80" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["api"], absolute := true } + (some #[("param1", some "value1"), ("param2", some "value2"), ("param3", some "value3")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/api?param1=value1¶m2=value2¶m3=value3" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["search"], absolute := true } + (some #[("debug", none), ("verbose", none), ("q", some "test")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/search?debug&verbose&q=test" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["api"], absolute := true } + (some #[("empty", some ""), ("also_empty", some ""), ("has_value", some "something")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/api?empty=&also_empty=&has_value=something" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["search"], absolute := true } + (some #[("q", some "cats&dogs"), ("filter", some "name=max")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/search?q=cats%26dogs&filter=name%3Dmax" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #[""], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["api", "v1", "users", "123", "posts", "456", "comments", "789"], absolute := true } + none + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/api/v1/users/123/posts/456/comments/789" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #["files", "..", "etc", "passwd"], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/files/../etc/passwd" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #["path/with/encoded/slashes"], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/path%2Fwith%2Fencoded%2Fslashes" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.authorityForm + { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := some 8080 } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "example.com:8080" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := some 8080 }, + path := { segments := #["ata"], absolute := true }, + query := none, + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://example.com:8080/ata" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.URI.Host.ipv4 192.168.1.1, port := some 3000 } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "192.168.1.1:3000" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.URI.Host.ipv6 ::1, port := some 8080 } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "[::1]:8080" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "http", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := none }, + path := { segments := #["path", "to", "resource"], absolute := true }, + query := some #[("query", some "value")], + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "http://example.com/path/to/resource?query=value" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "api.example.com", port := some 443 }, + path := { segments := #["v1", "users"], absolute := true }, + query := some #[("limit", some "10")], + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://api.example.com:443/v1/users?limit=10" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := some "user:pass", + host := Std.Http.URI.Host.name "secure.example.com", + port := none }, + path := { segments := #["private"], absolute := true }, + query := none, + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://user:pass@secure.example.com/private" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "http", + authority := some { userInfo := none, host := Std.Http.URI.Host.ipv6 2001:db8::1, port := some 8080 }, + path := { segments := #["path"], absolute := true }, + query := none, + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "http://[2001:db8::1]:8080/path" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := none }, + path := { segments := #["page"], absolute := true }, + query := none, + fragment := some "section1" } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://example.com/page#section1" + IO.println (repr result) + +/-- +error: offset 0: invalid request target +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "?query=only" + IO.println (repr result) + +/-- +error: offset 1: it's a scheme starter +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "//double//slash//path" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["very", "long", "path", "with", "many", "segments", "and", "encoded spaces", "and+plus+signs", + "final/segment"], + absolute := true } + none + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/very/long/path/with/many/segments/and/encoded%20spaces/and%2Bplus%2Bsigns/final%2Fsegment" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm + { segments := #["api"], absolute := true } + (some #[("filters[]", some "active"), ("filters[]", some "verified"), ("sort[name]", some "asc"), + ("sort[date]", some "desc")]) + none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/api?filters%5B%5D=active&filters%5B%5D=verified&sort%5Bname%5D=asc&sort%5Bdate%5D=desc" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.absoluteForm + { scheme := "https", + authority := some { userInfo := none, host := Std.Http.URI.Host.name "xn--nxasmq6b.xn--o3cw4h", port := none }, + path := { segments := #["path"], absolute := true }, + query := none, + fragment := none } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "https://xn--nxasmq6b.xn--o3cw4h/path" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.authorityForm + { userInfo := none, host := Std.Http.URI.Host.name "localhost", port := some 65535 } +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "localhost:65535" + IO.println (repr result) + +/-- +info: Std.Http.RequestTarget.originForm { segments := #[""], absolute := true } none none +-/ +#guard_msgs in +#eval show IO _ from do + let result ← runParser Std.Http.Parser.parseRequestTarget "/" + IO.println (repr result) diff --git a/tests/lean/run/async_simple_http.lean b/tests/lean/run/async_simple_http.lean new file mode 100644 index 000000000000..3bc435df7da2 --- /dev/null +++ b/tests/lean/run/async_simple_http.lean @@ -0,0 +1,296 @@ +import Std.Internal.Http +import Std.Internal.Async + +open Std.Internal.IO.Async +open Std Http + +structure Result where + responseSent : Nat + data : ByteArray + +def sendraw (client : Server.Mock.Client) (reqs: Array ByteArray) (onRequest : Request Body → Async (Response Body)) : IO ByteArray := Async.block do + for req in reqs do + client.enqueueReceive req + + Std.Http.Server.serveConnection client onRequest (config := { lingeringTimeout := 3000 }) + + client.getSentData + +def sendRequests (client : Server.Mock.Client) (reqs : Array (Request (Array String))) (onRequest : Request Body → Async (Response Body)) : IO ByteArray := Async.block do + for req in reqs do + client.enqueueReceive <| String.toUTF8 <| toString req.head + for part in req.body do client.enqueueReceive <| part.toUTF8 + + Std.Http.Server.serveConnection client onRequest (config := { lingeringTimeout := 3000 }) + + client.getSentData + +def testSizeLimit (client : Server.Mock.Client) : IO Unit := do + let handler := fun (req : Request Body) => do + let mut size := 0 + for i in req.body do + size := size + i.size + if size > 10 then return Response.new |>.status .payloadTooLarge |>.build + + return Response.new + |>.status .ok + |>.body "hello robert" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/ata/po" + |>.header "Content-Length" (.new "4") + |>.header "Host" (.new ".") + |>.body #["debg"], + Request.new + |>.uri! "/ata/po" + |>.header "Content-Length" (.new "13") + |>.header "Connection" (.new "close") + |>.header "Host" (.new ".") + |>.body #["debgadsadsads"], + Request.new + |>.uri! "/ata/po" + |>.header "Content-Length" (.new "4") + |>.header "Host" (.new ".") + |>.body #["debg"], + ] handler + + let responseData := String.fromUTF8! response + IO.println <| String.quote responseData + +/-- +info: "HTTP/1.1 200 OK\x0d\nContent-Length: 12\x0d\nServer: LeanHTTP/1.1\x0d\n\x0d\nhello robertHTTP/1.1 413 Request Entity Too Large\x0d\nConnection: close\x0d\nServer: LeanHTTP/1.1\x0d\n\x0d\n" +-/ +#guard_msgs in +#eval show IO _ from do testSizeLimit (← Server.Mock.Client.new) + +def testBasicRequest : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (_ : Request Body) => do + return Response.new + |>.status .ok + |>.header "Custom-Header" (.new "test-value") + |>.body "Hello World" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/hello" + |>.header "Host" (.new "localhost") + |>.header "User-Agent" (.new "TestClient/1.0") + |>.header "Connection" (.new "close") + |>.header "Content-Length" (.new "0") + |>.method .get + |>.body #[""] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +/-- +info: "HTTP/1.1 200 OK\x0d\nContent-Length: 11\x0d\nConnection: close\x0d\nCustom-Header: test-value\x0d\nServer: LeanHTTP/1.1\x0d\n\x0d\nHello World" +-/ +#guard_msgs in +#eval show IO _ from do testBasicRequest +def testPostRequest : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (req : Request Body) => do + let mut body := "" + for chunk in req.body do + body := body ++ String.fromUTF8! chunk + + return Response.new + |>.status .ok + |>.header "Content-Type" (.new "application/json") + |>.body s!"Received: {body}" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/api/data" + |>.method .post + |>.header "Host" (.new "localhost") + |>.header "Content-Type" (.new "application/json") + |>.header "Content-Length" (.new "25") + |>.header "Connection" (.new "close") + |>.body #["{\"name\": \"test\", \"id\": 1}"] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +def test100Continue : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (req : Request Body) => do + let expectHeader := req.head.headers.getLast? "Expect" |>.getD (.new "") + if expectHeader.is "100-continue" then + return Response.new + |>.status .continue + |>.build + else + return Response.new + |>.status .ok + |>.body "Request processed" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/" + |>.method .get + |>.header "Host" (.new "example.com") + |>.header "Content-Length" (.new "1") + |>.header "Expect" (.new "100-continue") + |>.header "Connection" (.new "close") + |>.body #["a"] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +/-- +info: "HTTP/1.1 100 Continue\x0d\nConnection: close\x0d\nServer: LeanHTTP/1.1\x0d\n\x0d\n" +-/ +#guard_msgs in +#eval show IO _ from do test100Continue + +def testMaxRequestSize : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (req : Request Body) => do + let mut totalSize := 0 + for chunk in req.body do + totalSize := totalSize + chunk.size + if totalSize > 1000 then + return Response.new + |>.status .payloadTooLarge + |>.header "Content-Type" (.new "application/json") + |>.body "{\"error\": \"Request too large\", \"max_size\": 1000}" + + return Response.new + |>.status .ok + |>.body s!"Accepted request of size {totalSize}" + + let largeData := + Array.replicate 1500 97 + |> ByteArray.mk + |> String.fromUTF8! + + let response ← sendRequests client #[ + Request.new + |>.uri! "/upload" + |>.method .post + |>.header "Host" (.new "localhost") + |>.header "Content-Type" (.new "text/plain") + |>.header "Content-Length" (.ofString! s!"{largeData.length}") + |>.header "Connection" (.new "close") + |>.body #[largeData] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +/-- +info: "HTTP/1.1 413 Request Entity Too Large\x0d\nContent-Length: 48\x0d\nConnection: close\x0d\nServer: LeanHTTP/1.1\x0d\nContent-Type: application/json\x0d\n\x0d\n{\"error\": \"Request too large\", \"max_size\": 1000}" +-/ +#guard_msgs in +#eval show IO _ from do testMaxRequestSize + +/-- +info: "HTTP/1.1 200 OK\x0d\nContent-Length: 35\x0d\nConnection: close\x0d\nServer: LeanHTTP/1.1\x0d\nContent-Type: application/json\x0d\n\x0d\nReceived: {\"name\": \"test\", \"id\": 1}" +-/ +#guard_msgs in +#eval show IO _ from do testPostRequest + +def testContentNegotiation : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (req : Request Body) => do + if req.head.headers.hasEntry "Accept" "application/json" then + return Response.new + |>.status .accepted + |>.header "Content-Type" (.new "application/json") + |>.body "{\"message\": \"JSON response\", \"status\": \"accepted\"}" + else if req.head.headers.hasEntry "Accept" "text/xml" then + return Response.new + |>.status .ok + |>.header "Content-Type" (.new "application/xml") + |>.body "XML response" + else + return Response.new + |>.status .ok + |>.header "Content-Type" (.new "text/plain") + |>.body "Plain text response" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/api/content" + |>.method .post + |>.header "Host" (.new "localhost") + |>.header "Accept" (.new "application/json") + |>.header "Content-Type" (.new "application/json") + |>.header "Content-Length" (.new "19") + |>.body #["{\"request\": \"data\"}"], + Request.new + |>.uri! "/api/content" + |>.method .get + |>.header "Host" (.new "localhost") + |>.header "Accept" (.new "text/xml") + |>.header "Content-Length" (.new "1") + |>.body #["a"] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +/-- +info: "HTTP/1.1 202 Accepted\x0d\nContent-Length: 50\x0d\nServer: LeanHTTP/1.1\x0d\nContent-Type: application/json\x0d\n\x0d\n{\"message\": \"JSON response\", \"status\": \"accepted\"}HTTP/1.1 200 OK\x0d\nContent-Length: 73\x0d\nServer: LeanHTTP/1.1\x0d\nContent-Type: application/xml\x0d\n\x0d\nXML response" +-/ +#guard_msgs in +#eval show IO _ from do testContentNegotiation + +def testContentNegotiationError : IO Unit := do + let client ← Server.Mock.Client.new + + let handler := fun (req : Request Body) => do + if req.head.headers.hasEntry "Accept" "application/json" then + return Response.new + |>.status .accepted + |>.header "Content-Type" (.new "application/json") + |>.body "{\"message\": \"JSON response\", \"status\": \"accepted\"}" + else if req.head.headers.hasEntry "Accept" "text/xml" then + return Response.new + |>.status .ok + |>.header "Content-Type" (.new "application/xml") + |>.body "XML response" + else + return Response.new + |>.status .ok + |>.header "Content-Type" (.new "text/plain") + |>.body "Plain text response" + + let response ← sendRequests client #[ + Request.new + |>.uri! "/api/content" + |>.method .post + |>.header "Host" (.new "localhost") + |>.header "Accept" (.new "application/json") + |>.header "Content-Type" (.new "application/json") + |>.header "Content-Length" (.new "18") + |>.body #["{\"request\": \"data\"}"], + Request.new + |>.uri! "/api/content" + |>.method .get + |>.header "Host" (.new "localhost") + |>.header "Accept" (.new "text/xml") + |>.header "Content-Length" (.new "1") + |>.body #["a"] + ] handler + + let responseData := String.fromUTF8! response + IO.println s!"{responseData.quote}" + +/-- +info: "HTTP/1.1 202 Accepted\x0d\nContent-Length: 50\x0d\nServer: LeanHTTP/1.1\x0d\nContent-Type: application/json\x0d\n\x0d\n{\"message\": \"JSON response\", \"status\": \"accepted\"}HTTP/1.1 400 Bad Request\x0d\nConnection: close\x0d\nServer: LeanHTTP/1.1\x0d\n\x0d\n" +-/ +#guard_msgs in +#eval show IO _ from do testContentNegotiationError