diff --git a/src/Std/Internal.lean b/src/Std/Internal.lean index 4aac6fd85c..db530bc593 100644 --- a/src/Std/Internal.lean +++ b/src/Std/Internal.lean @@ -7,6 +7,7 @@ module prelude public import Std.Internal.Async +public import Std.Internal.Http public import Std.Internal.Parsec public import Std.Internal.UV diff --git a/src/Std/Internal/Http.lean b/src/Std/Internal/Http.lean new file mode 100644 index 0000000000..1dc3c0b6ad --- /dev/null +++ b/src/Std/Internal/Http.lean @@ -0,0 +1,9 @@ +/- +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 diff --git a/src/Std/Internal/Http/Data.lean b/src/Std/Internal/Http/Data.lean new file mode 100644 index 0000000000..5c0586b828 --- /dev/null +++ b/src/Std/Internal/Http/Data.lean @@ -0,0 +1,21 @@ +/- +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.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.Status +public import Std.Internal.Http.Data.Chunk + +/-! +# HTTP Data Types + +This module re-exports all HTTP data types including request/response structures, +methods, status codes, chunks, and extension metadata. +-/ diff --git a/src/Std/Internal/Http/Data/Chunk.lean b/src/Std/Internal/Http/Data/Chunk.lean new file mode 100644 index 0000000000..c6efd8740e --- /dev/null +++ b/src/Std/Internal/Http/Data/Chunk.lean @@ -0,0 +1,210 @@ +/- +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.Internal +public meta import Std.Internal.Http.Internal.String + +public section + +/-! +# Chunk + +This module defines the `Chunk` type, which represents a chunk of data from a request or response. + +Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-7.1 +-/ + +namespace Std.Http + +open Internal + +set_option linter.all true + +namespace Chunk + +/-- +A proposition stating that `s` is a valid chunk-extension name: every character in `s` is an +HTTP token character and `s` is non-empty. + +Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension +-/ +abbrev IsValidExtensionName (s : String) : Prop := + isToken s + +/-- +A validated chunk extension name that ensures all characters conform to HTTP standards +per RFC 9112 §7.1.1. Extension names appear in chunked transfer encoding as key-value metadata. + +Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension +-/ +structure ExtensionName where + /-- + The extension name string. + -/ + value : String + + /-- + The proof that it's a valid extension name. + -/ + isValidExtensionName : IsValidExtensionName value := by decide +deriving Repr, DecidableEq, BEq + +instance : Hashable ExtensionName where + hash x := Hashable.hash x.value + +instance : Inhabited ExtensionName where + default := ⟨"_", by decide⟩ + +instance : ToString ExtensionName where + toString name := name.value + +namespace ExtensionName + +/-- +Attempts to create an `ExtensionName` from a `String`, returning `none` if the string contains +invalid characters or is empty. +-/ +def ofString? (s : String) : Option ExtensionName := + if h : IsValidExtensionName s then + some ⟨s, h⟩ + else + none + +/-- +Creates an `ExtensionName` from a string, panicking with an error message if the string contains +invalid characters or is empty. +-/ +def ofString! (s : String) : ExtensionName := + match ofString? s with + | some res => res + | none => panic! ("invalid extension name: " ++ s.quote) + +end ExtensionName + +/-- +A proposition asserting that `s` is a valid extension value, meaning it can be correctly encoded and +decoded as either a token or a quoted-string. + +Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension +-/ +abbrev IsValidExtensionValue (s : String) : Prop := + (quoteHttpString? s).isSome + +/-- +A validated chunk extension value that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1. +Extension values appear in chunked transfer encoding as metadata associated with extension names. + +Note: UTF-8 encoding is not supported. The quoting mechanism is strict and only permits escaping +specific values. Additionally, the library does not support obs-text, which means certain UTF-8 +characters or values outside of token, qdtext, and the limited set of escapable characters cannot be +encoded. + +Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension +-/ +structure ExtensionValue where + /-- + The extension value string. + -/ + value : String + + /-- + The proof that it's a valid extension value. + -/ + validExtensionValue : IsValidExtensionValue value := by decide +deriving Repr, DecidableEq, BEq + +namespace ExtensionValue + +instance : Inhabited ExtensionValue where + default := ⟨"", by native_decide⟩ + +instance : ToString ExtensionValue where + toString v := v.value + +/-- +Quotes an extension value if it contains non-token characters, otherwise returns it as-is. + +-/ +def quote (s : ExtensionValue) : String := + quoteHttpString? s.value |>.get s.validExtensionValue + +/-- +Attempts to create an `ExtensionValue` from a `String`, returning `none` if the string contains +characters that cannot be encoded as an HTTP quoted-string. +-/ +def ofString? (s : String) : Option ExtensionValue := + if h : (quoteHttpString? s).isSome then + some ⟨s, h⟩ + else + none + +/-- +Creates an `ExtensionValue` from a string, panicking with an error message if the string contains +characters that cannot be encoded as an HTTP quoted-string. +-/ +def ofString! (s : String) : ExtensionValue := + match ofString? s with + | some res => res + | none => panic! ("invalid extension value: " ++ s.quote) + +end Chunk.ExtensionValue + +/-- +Represents a chunk of data with optional extensions (key-value pairs). + +Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.7.1 +-/ +structure Chunk where + + /-- + The byte data contained in this chunk. + -/ + data : ByteArray + + /-- + Optional metadata associated with this chunk as key-value pairs. Keys are validated + `Chunk.ExtensionName` values, values are optional strings. + -/ + extensions : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue) := #[] +deriving Inhabited + +namespace Chunk + +/-- +An empty chunk with no data and no extensions. +-/ +def empty : Chunk := + { data := .empty, extensions := #[] } + +/-- +Creates a simple chunk without extensions. +-/ +def ofByteArray (data : ByteArray) : Chunk := + { data := data, extensions := #[] } + +/-- +Adds an extension to a chunk. +-/ +def insertExtension (chunk : Chunk) (key : Chunk.ExtensionName) (value : ExtensionValue) : Chunk := + { chunk with extensions := chunk.extensions.push (key, some value) } + +/-- +Interprets the chunk data as a UTF-8 encoded string. +-/ +def toString? (chunk : Chunk) : Option String := + String.fromUTF8? chunk.data + +instance : Encode .v11 Chunk where + encode buffer chunk := + let chunkLen := chunk.data.size + let exts := chunk.extensions.foldl (fun acc (name, value) => + acc ++ ";" ++ name.value ++ (value.elim "" (fun x => "=" ++ x.quote))) "" + let size := Nat.toDigits 16 chunkLen |>.toArray |>.map Char.toUInt8 |> ByteArray.mk + buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8] + +end Chunk diff --git a/src/Std/Internal/Http/Data/Extensions.lean b/src/Std/Internal/Http/Data/Extensions.lean new file mode 100644 index 0000000000..b21708bcdd --- /dev/null +++ b/src/Std/Internal/Http/Data/Extensions.lean @@ -0,0 +1,104 @@ +/- +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.Dynamic +public import Init.Data.String +public import Std.Data.TreeMap + +open Lean + +public section + +/-! +# Extensions + +This module provides the `Extensions` type, a dynamically-typed map for storing metadata on HTTP +requests and responses. It can be used by parsers, middleware, or other processing stages +to attach arbitrary typed data. +-/ + +namespace Std.Http + +set_option linter.all true + +/- +`quickCmp` is unavailable here, so this is a simpler implementation of the same comparison. +-/ + +/-- +An ordering for `Name` keys used by `Extensions`. +-/ +protected def Extensions.compareName : Name → Name → Ordering + | .anonymous, .anonymous => .eq + | .anonymous, _ => .lt + | _, .anonymous => .gt + | .str p₁ s₁, .str p₂ s₂ => + match Extensions.compareName p₁ p₂ with + | .eq => compareOfLessAndEq s₁ s₂ + | ord => ord + | .str _ _, .num _ _ => .lt + | .num _ _, .str _ _ => .gt + | .num p₁ n₁, .num p₂ n₂ => + match Extensions.compareName p₁ p₂ with + | .eq => compare n₁ n₂ + | ord => ord + +/-- +A dynamically typed map for optional metadata that can be attached to HTTP requests and responses. +Extensions allow storing arbitrary typed data keyed by type name, useful for metadata such as socket +information or custom processing data. +-/ +structure Extensions where + private mk :: + + /-- + The underlying tree map storing dynamic values keyed by their type name. + -/ + private data : TreeMap Name Dynamic Extensions.compareName := .empty +deriving Inhabited + +namespace Extensions + +/-- +An empty extensions map with no data. +-/ +def empty : Extensions := + ⟨.empty⟩ + +/-- +Retrieves a value of type `α` from the extensions, if present. +-/ +@[inline] +def get (x : Extensions) (α : Type) [TypeName α] : Option α := do + let dyn ← x.data.get? (TypeName.typeName α) + dyn.get? α + +/-- +Inserts a value into the extensions, keyed by its type name. If a value of the same type already +exists, it is replaced. +-/ +@[inline] +def insert (x : Extensions) [TypeName α] (data : α) : Extensions := + let dyn := Dynamic.mk data + ⟨x.data.insert dyn.typeName dyn⟩ + +/-- +Removes the value of type `α` from the extensions. +-/ +@[inline] +def remove (x : Extensions) (α : Type) [TypeName α] : Extensions := + ⟨x.data.erase (TypeName.typeName α)⟩ + +/-- +Checks whether the extensions contain a value of type `α`. +-/ +@[inline] +def contains (x : Extensions) (α : Type) [TypeName α] : Bool := + x.data.contains (TypeName.typeName α) + +end Std.Http.Extensions diff --git a/src/Std/Internal/Http/Data/Method.lean b/src/Std/Internal/Http/Data/Method.lean new file mode 100644 index 0000000000..f01c1b560f --- /dev/null +++ b/src/Std/Internal/Http/Data/Method.lean @@ -0,0 +1,385 @@ +/- +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.ToString +public import Std.Internal.Http.Internal + +public section + +/-! +# Method + +This module provides the `Method` type that represents HTTP request methods. It defines all +IANA-registered HTTP methods as distinct constructors, including standard methods (e.g. `GET`, +`POST`, `PUT`, `DELETE`) and extension methods from WebDAV, CalDAV, and other specifications. +Unrecognized method strings produce `none` from `ofString?`. + +References: +* https://httpwg.org/specs/rfc9112.html#request.method +* https://httpwg.org/specs/rfc9110.html#method.overview +* https://www.iana.org/assignments/http-methods/http-methods.xhtml +-/ + +namespace Std.Http + +set_option linter.all true + +open Internal + +/-- +A method is a verb that describes the action to be performed. + +Covers all methods in the IANA HTTP Method Registry. + +* Reference: https://www.iana.org/assignments/http-methods/http-methods.xhtml +-/ +inductive Method where + /-- + Access control list for a resource. + Source: https://www.rfc-editor.org/rfc/rfc3744#section-8.1 + -/ + | acl + + /-- + Apply a label to a version-controlled resource baseline. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-12.6 + -/ + | baselineControl + + /-- + Bind a resource to an additional URI path. + Source: https://www.rfc-editor.org/rfc/rfc5842#section-4 + -/ + | bind + + /-- + Check in a checked-out version-controlled resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-9.4 + -/ + | checkin + + /-- + Check out a version-controlled resource for modification. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.8 + -/ + | checkout + + /-- + Establish a tunnel to a server (often for TLS). + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.6 + -/ + | connect + + /-- + Copy a resource to a new URI. + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.8 + -/ + | copy + + /-- + Remove a resource. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.5 + -/ + | delete + + /-- + Retrieve a resource. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.1 + -/ + | get + + /-- + Retrieve headers for a resource, without the body. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.2 + -/ + | head + + /-- + Apply a label to a version history. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.2 + -/ + | label + + /-- + Create a link relationship between resources. + Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.2 + -/ + | link + + /-- + Lock a resource to prevent concurrent modifications. + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.10 + -/ + | lock + + /-- + Merge a version-controlled resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-11.2 + -/ + | merge + + /-- + Create a new activity resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-13.5 + -/ + | mkactivity + + /-- + Create a calendar collection. + Source: https://www.rfc-editor.org/rfc/rfc4791#section-5.3.1 + -/ + | mkcalendar + + /-- + Create a collection resource (WebDAV directory). + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.3 + -/ + | mkcol + + /-- + Create a redirect reference resource. + Source: https://www.rfc-editor.org/rfc/rfc4437#section-6 + -/ + | mkredirectref + + /-- + Create a workspace resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-6.3 + -/ + | mkworkspace + + /-- + Move a resource to a new URI. + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.9 + -/ + | move + + /-- + Describe communication options for a resource. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.7 + -/ + | options + + /-- + Reorder members of a collection. + Source: https://www.rfc-editor.org/rfc/rfc3648#section-7 + -/ + | orderpatch + + /-- + Apply partial modifications to a resource. + Source: https://www.rfc-editor.org/rfc/rfc5789#section-2 + -/ + | patch + + /-- + Submit data to be processed (e.g., form submission). + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.3 + -/ + | post + + /-- + HTTP/2 connection preface (not used in application code). + Source: https://www.rfc-editor.org/rfc/rfc9113#section-3.4 + -/ + | pri + + /-- + Retrieve properties of a resource (WebDAV). + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.1 + -/ + | propfind + + /-- + Set or remove properties on a resource (WebDAV). + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.2 + -/ + | proppatch + + /-- + Replace a resource with new data. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.4 + -/ + | put + + /-- + Perform a safe query with a request body. + Source: https://www.ietf.org/archive/id/draft-ietf-httpbis-safe-method-w-body-14.html#section-2 + -/ + | query + + /-- + Rebind a resource to a new URI path. + Source: https://www.rfc-editor.org/rfc/rfc5842#section-6 + -/ + | rebind + + /-- + Retrieve a report on a resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.6 + -/ + | report + + /-- + Search a resource. + Source: https://www.rfc-editor.org/rfc/rfc5323#section-2 + -/ + | search + + /-- + Perform a message loop-back test. + Source: https://httpwg.org/specs/rfc9110.html#section-9.3.8 + -/ + | trace + + /-- + Remove a URI binding from a resource. + Source: https://www.rfc-editor.org/rfc/rfc5842#section-5 + -/ + | unbind + + /-- + Undo a previous checkout of a version-controlled resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-4.5 + -/ + | uncheckout + + /-- + Remove a link relationship between resources. + Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.3 + -/ + | unlink + + /-- + Unlock a resource. + Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.11 + -/ + | unlock + + /-- + Update a version-controlled resource. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-7.1 + -/ + | update + + /-- + Update a redirect reference resource. + Source: https://www.rfc-editor.org/rfc/rfc4437#section-7 + -/ + | updateredirectref + + /-- + Put a resource under version control. + Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.5 + -/ + | versionControl +deriving Repr, Inhabited, BEq, DecidableEq + +namespace Method + +/-- +Converts a `String` into a `Method`. Returns `none` for unrecognized method strings. +-/ +def ofString? : String → Option Method + | "ACL" => some .acl + | "BASELINE-CONTROL" => some .baselineControl + | "BIND" => some .bind + | "CHECKIN" => some .checkin + | "CHECKOUT" => some .checkout + | "CONNECT" => some .connect + | "COPY" => some .copy + | "DELETE" => some .delete + | "GET" => some .get + | "HEAD" => some .head + | "LABEL" => some .label + | "LINK" => some .link + | "LOCK" => some .lock + | "MERGE" => some .merge + | "MKACTIVITY" => some .mkactivity + | "MKCALENDAR" => some .mkcalendar + | "MKCOL" => some .mkcol + | "MKREDIRECTREF" => some .mkredirectref + | "MKWORKSPACE" => some .mkworkspace + | "MOVE" => some .move + | "OPTIONS" => some .options + | "ORDERPATCH" => some .orderpatch + | "PATCH" => some .patch + | "POST" => some .post + | "PRI" => some .pri + | "PROPFIND" => some .propfind + | "PROPPATCH" => some .proppatch + | "PUT" => some .put + | "QUERY" => some .query + | "REBIND" => some .rebind + | "REPORT" => some .report + | "SEARCH" => some .search + | "TRACE" => some .trace + | "UNBIND" => some .unbind + | "UNCHECKOUT" => some .uncheckout + | "UNLINK" => some .unlink + | "UNLOCK" => some .unlock + | "UPDATE" => some .update + | "UPDATEREDIRECTREF" => some .updateredirectref + | "VERSION-CONTROL" => some .versionControl + | _ => none + +/-- +Converts a `String` into a `Method`, panicking if unrecognized. +-/ +def ofString! (s : String) : Method := + match ofString? s with + | some m => m + | none => panic! s!"invalid HTTP method: {s.quote}" + +instance : ToString Method where + toString + | .acl => "ACL" + | .baselineControl => "BASELINE-CONTROL" + | .bind => "BIND" + | .checkin => "CHECKIN" + | .checkout => "CHECKOUT" + | .connect => "CONNECT" + | .copy => "COPY" + | .delete => "DELETE" + | .get => "GET" + | .head => "HEAD" + | .label => "LABEL" + | .link => "LINK" + | .lock => "LOCK" + | .merge => "MERGE" + | .mkactivity => "MKACTIVITY" + | .mkcalendar => "MKCALENDAR" + | .mkcol => "MKCOL" + | .mkredirectref => "MKREDIRECTREF" + | .mkworkspace => "MKWORKSPACE" + | .move => "MOVE" + | .options => "OPTIONS" + | .orderpatch => "ORDERPATCH" + | .patch => "PATCH" + | .post => "POST" + | .pri => "PRI" + | .propfind => "PROPFIND" + | .proppatch => "PROPPATCH" + | .put => "PUT" + | .query => "QUERY" + | .rebind => "REBIND" + | .report => "REPORT" + | .search => "SEARCH" + | .trace => "TRACE" + | .unbind => "UNBIND" + | .uncheckout => "UNCHECKOUT" + | .unlink => "UNLINK" + | .unlock => "UNLOCK" + | .update => "UPDATE" + | .updateredirectref => "UPDATEREDIRECTREF" + | .versionControl => "VERSION-CONTROL" + +instance : Encode .v11 Method where + encode buffer := buffer.writeString ∘ toString + +end Std.Http.Method diff --git a/src/Std/Internal/Http/Data/Request.lean b/src/Std/Internal/Http/Data/Request.lean new file mode 100644 index 0000000000..d03ceca092 --- /dev/null +++ b/src/Std/Internal/Http/Data/Request.lean @@ -0,0 +1,228 @@ +/- +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.Extensions +public import Std.Internal.Http.Data.Method +public import Std.Internal.Http.Data.Version + +public section + +/-! +# Request + +This module provides the `Request` type, which represents an HTTP request. It also defines ways +to build a `Request` using functions that make it easier. + +References: +* https://httpwg.org/specs/rfc9112.html#request.line +-/ + +namespace Std.Http + +set_option linter.all true + +/-- +The main parts of a request containing the HTTP method, version, and request target URI. + +Reference: https://httpwg.org/specs/rfc9112.html#request.line +-/ +structure Request.Head where + /-- + The HTTP method (GET, POST, PUT, DELETE, etc.) for the request + + Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.3.1 + -/ + method : Method + + /-- + The HTTP protocol version for the request (e.g. HTTP/1.1, HTTP/2.0, HTTP/3.0). + + Reference: https://httpwg.org/specs/rfc9112.html#http.version + -/ + version : Version + + /-- + The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form). + -/ + uri : String +deriving Inhabited, Repr + +/-- +HTTP request structure parameterized by body type. +-/ +structure Request (t : Type) where + /-- + The request line information (`method`, `version`, and request-target `uri`). + -/ + line : Request.Head + + /-- + The request body content of type t. + -/ + body : t + + /-- + Optional dynamic metadata attached to the request. + -/ + extensions : Extensions := .empty +deriving Inhabited + +/-- +Builds an HTTP Request. +-/ +structure Request.Builder where + /-- + The request-line of an HTTP request. + -/ + line : Head := { method := .get, version := .v11, uri := "*" } + + /-- + Optional dynamic metadata attached to the request. + -/ + extensions : Extensions := .empty + +namespace Request + +instance : ToString Head where + toString req := + toString req.method ++ " " ++ + toString req.uri ++ " " ++ + toString req.version ++ + "\r\n" + +open Internal in +instance : Encode .v11 Head where + encode buffer req := + let buffer := Encode.encode (v := .v11) buffer req.method + let buffer := buffer.writeChar ' ' + let buffer := buffer.writeString req.uri + let buffer := buffer.writeChar ' ' + let buffer := Encode.encode (v := .v11) buffer req.version + buffer.writeString "\r\n" + +/-- +Creates a new HTTP request builder with the default head +(method: GET, version: HTTP/1.1, target: `*`). +-/ +def new : Builder := { } + +namespace Builder + +/-- +Creates a new HTTP request builder with the default head +(method: GET, version: HTTP/1.1, target: `*`). +-/ +def empty : Builder := { } + +/-- +Sets the HTTP method for the request being built. +-/ +def method (builder : Builder) (method : Method) : Builder := + { builder with line := { builder.line with method := method } } + +/-- +Sets the HTTP version for the request being built. +-/ +def version (builder : Builder) (version : Version) : Builder := + { builder with line := { builder.line with version := version } } + +/-- +Sets the request target/URI for the request being built. +-/ +def uri (builder : Builder) (uri : String) : Builder := + { builder with line := { builder.line with uri := uri } } + +/-- +Inserts a typed extension value into the request being built. +-/ +def extension (builder : Builder) [TypeName α] (data : α) : Builder := + { builder with extensions := builder.extensions.insert data } + +/-- +Builds and returns the final HTTP Request with the specified body. +-/ +def body (builder : Builder) (body : t) : Request t := + { line := builder.line, body := body, extensions := builder.extensions } + +end Builder + +/-- +Creates a new HTTP GET Request with the specified URI. +-/ +def get (uri : String) : Builder := + new + |>.method .get + |>.uri uri + +/-- +Creates a new HTTP POST Request builder with the specified URI. +-/ +def post (uri : String) : Builder := + new + |>.method .post + |>.uri uri + +/-- +Creates a new HTTP PUT Request builder with the specified URI. +-/ +def put (uri : String) : Builder := + new + |>.method .put + |>.uri uri + +/-- +Creates a new HTTP DELETE Request builder with the specified URI. +-/ +def delete (uri : String) : Builder := + new + |>.method .delete + |>.uri uri + +/-- +Creates a new HTTP PATCH Request builder with the specified URI. +-/ +def patch (uri : String) : Builder := + new + |>.method .patch + |>.uri uri + +/-- +Creates a new HTTP HEAD Request builder with the specified URI. +-/ +def head (uri : String) : Builder := + new + |>.method .head + |>.uri uri + +/-- +Creates a new HTTP OPTIONS Request builder with the specified URI. +Use `Request.options "*"` for server-wide OPTIONS. +-/ +def options (uri : String) : Builder := + new + |>.method .options + |>.uri uri + +/-- +Creates a new HTTP CONNECT Request builder with the specified URI. +Typically used with authority-form URIs such as `"example.com:443"` for tunneling. +-/ +def connect (uri : String) : Builder := + new + |>.method .connect + |>.uri uri + +/-- +Creates a new HTTP TRACE Request builder with the specified URI. +-/ +def trace (uri : String) : Builder := + new + |>.method .trace + |>.uri uri + +end Std.Http.Request diff --git a/src/Std/Internal/Http/Data/Response.lean b/src/Std/Internal/Http/Data/Response.lean new file mode 100644 index 0000000000..fbc5b76f01 --- /dev/null +++ b/src/Std/Internal/Http/Data/Response.lean @@ -0,0 +1,198 @@ +/- +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.Extensions +public import Std.Internal.Http.Data.Status +public import Std.Internal.Http.Data.Version + +public section + +/-! +# Response + +This module provides the `Response` type, which represents an HTTP response. It also defines +builder functions for constructing responses and selecting common HTTP status codes. +-/ + +namespace Std.Http + +set_option linter.all true + +/-- +The main parts of a response. +-/ +structure Response.Head where + /-- + The HTTP status for the response. + -/ + status : Status := .ok + + /-- + The HTTP protocol version used in the response, e.g. `HTTP/1.1`. + -/ + version : Version := .v11 +deriving Inhabited, Repr + +/-- +HTTP response structure parameterized by body type. +-/ +structure Response (t : Type) where + /-- + The response status-line information. + -/ + line : Response.Head := {} + + /-- + The content of the response. + -/ + body : t + + /-- + Optional dynamic metadata attached to the response. + -/ + extensions : Extensions := .empty +deriving Inhabited + +/-- +Builds an HTTP Response. +-/ +structure Response.Builder where + /-- + The response status-line information. + -/ + line : Head := {} + + /-- + Optional dynamic metadata attached to the response. + -/ + extensions : Extensions := .empty + +namespace Response + +instance : ToString Head where + toString r := + toString r.version ++ " " ++ + toString r.status.toCode ++ " " ++ + r.status.reasonPhrase ++ "\r\n" + +open Internal in +instance : Encode .v11 Head where + encode buffer r := + let buffer := Encode.encode (v := .v11) buffer r.version + let buffer := buffer.writeChar ' ' + let buffer := buffer.writeString (toString r.status.toCode) + let buffer := buffer.writeChar ' ' + let buffer := buffer.writeString r.status.reasonPhrase + buffer.writeString "\r\n" + +/-- +Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1). +-/ +def new : Builder := { } + +namespace Builder + +/-- +Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1). +-/ +def empty : Builder := { } + +/-- +Sets the HTTP status code for the response being built. +-/ +def status (builder : Builder) (status : Status) : Builder := + { builder with line := { builder.line with status := status } } + +/-- +Inserts a typed extension value into the response being built. +-/ +def extension (builder : Builder) [TypeName α] (data : α) : Builder := + { builder with extensions := builder.extensions.insert data } + +/-- +Builds and returns the final HTTP Response with the specified body. +-/ +def body (builder : Builder) (body : t) : Response t := + { line := builder.line, body := body, extensions := builder.extensions } + +/-- +Builds and returns the final HTTP Response with an empty body (`{}`). +Requires an `EmptyCollection` instance for the response body type. +-/ +def build [EmptyCollection t] (builder : Builder) : Response t := + { line := builder.line, body := {}, extensions := builder.extensions } + +end Builder + +/-- +Creates a new HTTP Response builder with the 200 status code. +-/ +def ok : Builder := + .empty |>.status .ok + +/-- +Creates a new HTTP Response builder with the provided status. +-/ +def withStatus (status : Status) : Builder := + .empty |>.status status + +/-- +Creates a new HTTP Response builder with the 404 status code. +-/ +def notFound : Builder := + .empty |>.status .notFound + +/-- +Creates a new HTTP Response builder with the 500 status code. +-/ +def internalServerError : Builder := + .empty |>.status .internalServerError + +/-- +Creates a new HTTP Response builder with the 400 status code. +-/ +def badRequest : Builder := + .empty |>.status .badRequest + +/-- +Creates a new HTTP Response builder with the 201 status code. +-/ +def created : Builder := + .empty |>.status .created + +/-- +Creates a new HTTP Response builder with the 202 status code. +-/ +def accepted : Builder := + .empty |>.status .accepted + +/-- +Creates a new HTTP Response builder with the 401 status code. +-/ +def unauthorized : Builder := + .empty |>.status .unauthorized + +/-- +Creates a new HTTP Response builder with the 403 status code. +-/ +def forbidden : Builder := + .empty |>.status .forbidden + +/-- +Creates a new HTTP Response builder with the 409 status code. +-/ +def conflict : Builder := + .empty |>.status .conflict + +/-- +Creates a new HTTP Response builder with the 503 status code. +-/ +def serviceUnavailable : Builder := + .empty |>.status .serviceUnavailable + +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 0000000000..7263a57c29 --- /dev/null +++ b/src/Std/Internal/Http/Data/Status.lean @@ -0,0 +1,722 @@ +/- +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.Internal + +public section + +/-! +# Status + +This module defines the `Status` type, a representation of HTTP status codes. Status codes are +three-digit integer codes that describe the result of an HTTP request. This implementation +includes common named statuses and supports custom codes through `Status.other`. + +Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ + +namespace Std.Http + +set_option linter.all true + +open Internal + +/-- +A proposition stating that `s` is a valid HTTP reason phrase: every character passes +`Char.reasonPhraseChar` per RFC 9110 §15. + +Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase +-/ +abbrev IsValidReasonPhrase (s : String) : Prop := + s.toList.all Char.reasonPhraseChar + +/-- +Returns `true` for every status code that has a dedicated named constructor in `Status`. +Used to ensure `Status.other` is never constructed with a code that already has a name. +-/ +def isKnownStatusCode (code: UInt16) : Bool := + code matches 100 | 101 | 102 | 103 + | 200 | 201 | 202 | 203 | 204 | 205 | 206 | 207 | 208 | 226 + | 300 | 301 | 302 | 303 | 304 | 305 | 306 | 307 | 308 + | 400 | 401 | 402 | 403 | 404 | 405 | 406 | 407 | 408 | 409 | 410 + | 411 | 412 | 413 | 414 | 415 | 416 | 417 | 418 | 421 | 422 | 423 + | 424 | 425 | 426 | 428 | 429 | 431 | 451 + | 500 | 501 | 502 | 503 | 504 | 505 | 506 | 507 | 508 | 510 | 511 + +/-- +A custom HTTP status with a numeric code and a reason phrase. Used to represent status codes +not enumerated as dedicated constructors in `Status`. The code must be in the range 100–999 +(a three-digit integer per RFC 9112 §4) and must not correspond to any named constructor. + +Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +structure CustomStatus where + + /-- + The numeric status code. + -/ + code : UInt16 + + /-- + The reason phrase associated with the status code. + -/ + phrase : String + + /-- + Proof that the reason phrase contains only valid characters. + -/ + validReasonPhrase : IsValidReasonPhrase phrase := by decide + + /-- + Proof that the code is a valid HTTP status code (100–999), i.e. a three-digit integer + as required by RFC 9112 §4. + -/ + validCode : 100 ≤ code ∧ code ≤ 999 := by decide + + /-- + Proof that the code does not clash with any named `Status` constructor. + -/ + validUnknown : ¬isKnownStatusCode code := by decide +deriving Repr, BEq + +instance : Inhabited CustomStatus where + default := ⟨209, "Unknown", by decide, by decide, by decide⟩ + +instance : ToString CustomStatus where + toString s := s.phrase + +namespace CustomStatus + +/-- +Attempts to create a `CustomStatus` from a numeric code and a reason phrase string, returning +`none` if the phrase contains invalid characters. +-/ +def ofCodeAndPhrase? (code : UInt16) (phrase : String) : Option CustomStatus := + if h : IsValidReasonPhrase phrase ∧ (100 ≤ code ∧ code ≤ 999) ∧ ¬isKnownStatusCode code then + some ⟨code, phrase, h.left, h.right.left, h.right.right⟩ + else + none + +end CustomStatus + +/-- +HTTP Status codes. Status codes are three-digit integer codes that describe the result of an +HTTP request. This implementation includes common named statuses and supports custom codes through +`Status.other`. + +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 + + /-- + A custom status code not covered by the standard constructors above. + -/ + | other (status : CustomStatus) +deriving Repr, Inhabited, BEq + +namespace Status + +/-- +Converts 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 + | other c => c.code + +/-- +Converts a `UInt16` to `Status`. +-/ +def ofCode (reasonPhrase : Option { x : String // IsValidReasonPhrase x }) (code: UInt16) : Option Status := + match h : code with + | 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 + | n => + let ph := reasonPhrase.getD ⟨"Unknown", by decide⟩ + + if h : (100 ≤ n ∧ n ≤ 999) ∧ ¬isKnownStatusCode n then + some <| .other ⟨n, ph.val, ph.property, h.left, h.right⟩ + else + none + +/-- +Checks if the type of the status code is informational, meaning that the request was received +and the process is continuing. + +Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isInformational (c : Status) : Bool := + 100 ≤ c.toCode ∧ c.toCode < 200 + +/-- +Checks if the status code is a success status, 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 + +/-- +Checks if the status code indicates an error (either client error 4xx or server error 5xx). + +Reference: https://httpwg.org/specs/rfc9110.html#status.codes +-/ +@[inline] +def isError (c : Status) : Bool := + c.isClientError ∨ c.isServerError + +/-- +Returns the standard reason phrase for an HTTP status code as defined in RFC 9110. +For known status codes this returns the canonical phrase (e.g., "OK" for 200). +For unknown codes (`other n s`), returns the caller-supplied reason phrase `s`. +-/ +def reasonPhrase : Status → String + | .«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 => "Payload Too Large" + | .uriTooLong => "URI Too Long" + | .unsupportedMediaType => "Unsupported Media Type" + | .rangeNotSatisfiable => "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" + | .other c => c.phrase + +instance : ToString Status where + toString := reasonPhrase + +instance : Encode .v11 Status where + encode buffer status := buffer + |>.writeString (toString <| toCode status) + |>.writeChar ' ' + |>.writeString status.reasonPhrase + +end Std.Http.Status diff --git a/src/Std/Internal/Http/Data/Version.lean b/src/Std/Internal/Http/Data/Version.lean new file mode 100644 index 0000000000..c3d08eef8e --- /dev/null +++ b/src/Std/Internal/Http/Data/Version.lean @@ -0,0 +1,99 @@ +/- +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 +import Init.Data.ToString +public import Init.Data.String + +public section + +/-! +# Version + +This module defines `Version`, the set of HTTP protocol versions modeled by this library. + +Reference: https://httpwg.org/specs/rfc9110.html#protocol.version +-/ + +namespace Std.Http + +set_option linter.all true + +/-- +HTTP protocol versions modeled by this library. + +Reference: https://httpwg.org/specs/rfc9110.html#protocol.version +-/ +inductive Version + /-- + `HTTP/1.0` + -/ + | v10 + + /-- + `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 ofNumber? : Nat → Nat → Option Version + | 1, 0 => some .v10 + | 1, 1 => some .v11 + | 2, 0 => some .v20 + | 3, 0 => some .v30 + | _, _ => none + +/-- +Converts `String` to the corresponding `Version`. +-/ +def ofString? : String → Option Version + | "HTTP/1.0" => some .v10 + | "HTTP/1.1" => some .v11 + | "HTTP/2.0" => some .v20 + | "HTTP/3.0" => some .v30 + | _ => none + +/-- +Converts `String` to the corresponding `Version`, panics if invalid. +-/ +def ofString! (s : String) : Version := + match ofString? s with + | some v => v + | none => panic! s!"invalid HTTP version: {s.quote}" + +/-- +Converts a `Version` to its corresponding major and minor numbers as a pair. +-/ +def toNumber : Version → (Nat × Nat) + | .v10 => (1, 0) + | .v11 => (1, 1) + | .v20 => (2, 0) + | .v30 => (3, 0) + +instance : ToString Version where + toString + | .v10 => "HTTP/1.0" + | .v11 => "HTTP/1.1" + | .v20 => "HTTP/2.0" + | .v30 => "HTTP/3.0" + +end Std.Http.Version diff --git a/src/Std/Internal/Http/Internal.lean b/src/Std/Internal/Http/Internal.lean new file mode 100644 index 0000000000..37386a86b4 --- /dev/null +++ b/src/Std/Internal/Http/Internal.lean @@ -0,0 +1,19 @@ +/- +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.Internal.ChunkedBuffer +public import Std.Internal.Http.Internal.Encode +public import Std.Internal.Http.Internal.String +public import Std.Internal.Http.Internal.Char + +/-! +# HTTP Internal Utilities + +This module re-exports internal utilities used by the HTTP library including +data structures, encoding functions, and buffer management. +-/ diff --git a/src/Std/Internal/Http/Internal/Char.lean b/src/Std/Internal/Http/Internal/Char.lean new file mode 100644 index 0000000000..6ff1589a3a --- /dev/null +++ b/src/Std/Internal/Http/Internal/Char.lean @@ -0,0 +1,281 @@ +/- +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 + +@[expose] +public section + +/-! +# HTTP Character Predicates + +This module provides shared character validation predicates used across the HTTP library. +All predicates in this module are ASCII-only by design (`isAscii c` where applicable), and +intentionally exclude `obs-text` and all non-ASCII code points. +-/ + +namespace Std.Http.Internal.Char + +set_option linter.all true + +/-- +Checks if a character is ASCII (Unicode code point < 128). +-/ +@[inline, expose] +def isAscii (c : Char) : Bool := + c.toNat < 128 + +/-- +Checks if a byte represents an ASCII character (value < 128). +-/ +@[inline, expose] +def isAsciiByte (c : UInt8) : Bool := + c < 128 + +/-- +Checks if a byte is a decimal digit (0-9). +-/ +@[inline, expose] +def isDigitByte (c : UInt8) : Bool := + c >= '0'.toUInt8 && c <= '9'.toUInt8 + +/-- +Checks if a byte is an alphabetic character (a-z or A-Z). +-/ +@[inline, expose] +def isAlphaByte (c : UInt8) : Bool := + (c >= 'A'.toUInt8 && c <= 'Z'.toUInt8) || (c >= 'a'.toUInt8 && c <= 'z'.toUInt8) + +/-- +tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*" + / "+" / "-" / "." / "^" / "_" / "`" / "|" / "~" + / DIGIT / ALPHA + ; Visible token characters used to build `token`. +-/ +@[inline] +def tchar (c : Char) : Bool := + (c matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' | '+' | '-' | '.' | '^' | '_' | '`' | '|' | '~') || + Char.isDigit c || + Char.isAlpha c + +/-- +vchar = %x21-7E +; Visible (printing) ASCII characters. +-/ +@[inline] +def vchar (c : Char) : Bool := + c ≥ '!' ∧ c ≤ '~' + +/-- +qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E +; ASCII-only variant (no obs-text). +-/ +@[inline] +def qdtext (c : Char) : Bool := + (c matches '\t' | ' ' | '!') || + ('#' ≤ c ∧ c ≤ '[') || + (']' ≤ c ∧ c ≤ '~') + +/-- +quoted-pair = "\\" ( HTAB / SP / VCHAR ) +; ASCII-only variant (no obs-text). +-/ +@[inline] +def quotedPairChar (c : Char) : Bool := + (c matches '\t' | ' ') || vchar c + +/-- +quoted-string body character class: +( qdtext / quoted-pair payload ) in ASCII-only mode. +-/ +@[inline] +def quotedStringChar (c : Char) : Bool := + qdtext c || quotedPairChar c + +/-- +field-vchar = VCHAR +; ASCII-only variant (no obs-text). +-/ +@[inline] +def fieldVchar (c : Char) : Bool := + vchar c + +/-- +field-content character class: +field-vchar / SP / HTAB +; ASCII-only variant (no obs-text). +-/ +@[inline] +def fieldContent (c : Char) : Bool := + fieldVchar c || (c matches ' ' | '\t') + +/-- +ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E +; ASCII-only variant (no obs-text). +-/ +@[inline] +def ctext (c : Char) : Bool := + (c matches '\t' | ' ') || + ('!' ≤ c ∧ c ≤ '\'') || + ('*' ≤ c ∧ c ≤ '[') || + (']' ≤ c ∧ c ≤ '~') + +/-- +etagc = "!" / %x23-7E +; ASCII-only variant (no obs-text). +-/ +@[inline] +def etagc (c : Char) : Bool := + c = '!' || ('#' ≤ c ∧ c ≤ '~') + +/-- +OWS = *( SP / HTAB ) (character class only) +-/ +@[inline] +def ows (c : Char) : Bool := + c matches ' ' | '\t' + +/-- +BWS = OWS (character class alias) +-/ +@[inline] +def bws (c : Char) : Bool := + ows c + +/-- +RWS = 1*( SP / HTAB ) (character class is identical to `ows`) +-/ +@[inline] +def rws (c : Char) : Bool := + ows c + +/-- +obs-text = %x80-FF (and higher Unicode scalar values in this library's `Char` model). +-/ +@[inline] +def obsText (c : Char) : Bool := + 0x80 ≤ c.toNat + +/-- +reason-phrase character class: +HTAB / SP / VCHAR +; ASCII-only variant (no obs-text). + +Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase +-/ +@[inline] +def reasonPhraseChar (c : Char) : Bool := + (c matches '\t' | ' ') || vchar c + +/-- +Checks if a character is a hexadecimal digit (0-9, a-f, or A-F). +-/ +@[inline, expose] +def isHexDigit (c : Char) : Bool := + (c matches 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') || + Char.isDigit c + +/-- +Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F). +-/ +@[inline, expose] +def isHexDigitByte (c : UInt8) : Bool := + (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) || + (c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) || + (c ≥ 'A'.toUInt8 && c ≤ 'F'.toUInt8) + +/-- +Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z). +-/ +@[inline, expose] +def isAlphaNum (c : UInt8) : Bool := + (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) || + (c ≥ 'a'.toUInt8 && c ≤ 'z'.toUInt8) || + (c ≥ 'A'.toUInt8 && c ≤ 'Z'.toUInt8) + +/-- +Checks whether `c` is an ASCII alphanumeric character. +-/ +@[inline, expose] +def isAsciiAlphaNumChar (c : Char) : Bool := + isAscii c && (Char.isDigit c || Char.isAlpha c) + +/-- +Checks if a character is valid after the first character of a URI scheme. +Valid characters are ASCII alphanumeric, `+`, `-`, and `.`. +-/ +@[inline, expose] +def isValidSchemeChar (c : Char) : Bool := + isAsciiAlphaNumChar c || (c matches '+' | '-' | '.') + +/-- +Checks if a character is valid for use in a domain name. +Valid characters are ASCII alphanumeric, hyphens, and dots. +-/ +@[inline, expose] +def isValidDomainNameChar (c : Char) : Bool := + isAsciiAlphaNumChar c || (c matches '-' | '.') + +/-- +Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are: +alphanumeric, hyphen, period, underscore, and tilde. +-/ +@[inline, expose] +def isUnreserved (c : UInt8) : Bool := + isAlphaNum c || + (c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8) + +/-- +Checks if a byte is a sub-delimiter character according to RFC 3986. +Sub-delimiters are: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`. +-/ +@[inline, expose] +def isSubDelims (c : UInt8) : Bool := + c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = ('\'' : Char).toUInt8 || + c = '('.toUInt8 || c = ')'.toUInt8 || c = '*'.toUInt8 || c = '+'.toUInt8 || + c = ','.toUInt8 || c = ';'.toUInt8 || c = '='.toUInt8 + +/-- +Checks if a byte is a valid path character (`pchar`) according to RFC 3986. +`pchar = unreserved / pct-encoded / sub-delims / ":" / "@"` + +Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`, +so this predicate only covers the non-percent characters. +-/ +@[inline, expose] +def isPChar (c : UInt8) : Bool := + isUnreserved c || isSubDelims c || c = ':'.toUInt8 || c = '@'.toUInt8 + +/-- +Checks if a byte is a valid character in a URI query component according to RFC 3986. +`query = *( pchar / "/" / "?" )` +-/ +@[inline, expose] +def isQueryChar (c : UInt8) : Bool := + isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8 + +/-- +Checks if a byte is a valid character in a URI fragment component according to RFC 3986. +`fragment = *( pchar / "/" / "?" )` +-/ +@[inline, expose] +def isFragmentChar (c : UInt8) : Bool := + isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8 + +/-- +Checks if a byte is a valid character in a URI userinfo component according to RFC 3986. +`userinfo = *( unreserved/ sub-delims / ":" )` + +Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean` +that provides it. +-/ +@[inline, expose] +def isUserInfoChar (c : UInt8) : Bool := + isUnreserved c || isSubDelims c || c = ':'.toUInt8 + +end Std.Http.Internal.Char diff --git a/src/Std/Internal/Http/Internal/ChunkedBuffer.lean b/src/Std/Internal/Http/Internal/ChunkedBuffer.lean new file mode 100644 index 0000000000..5f674bbbe2 --- /dev/null +++ b/src/Std/Internal/Http/Internal/ChunkedBuffer.lean @@ -0,0 +1,130 @@ +/- +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 +import Init.Data.ToString +import Init.Data.Array.Lemmas +public import Init.Data.String +public import Init.Data.ByteArray + +public section + +/-! +# ChunkedBuffer + +This module provides an efficient way to concatenate multiple `ByteArray`s by deferring the actual +concatenation until necessary. This is particularly useful in HTTP response building and streaming +scenarios where data is accumulated incrementally. +-/ + +namespace Std.Http.Internal + +set_option linter.all true + +/-- +A structure that accumulates multiple `ByteArray`s efficiently by tracking them in an array and +maintaining the total size. This allows building large buffers without repeated allocations and copies. +-/ +structure ChunkedBuffer where + /-- + The accumulated byte arrays. + -/ + data : Array ByteArray + + /-- + The total size in bytes of all accumulated arrays + -/ + size : Nat + +namespace ChunkedBuffer + +/-- +An empty `ChunkedBuffer`. +-/ +@[inline] +def empty : ChunkedBuffer := + { data := #[], size := 0 } + +/-- +Append a single `ByteArray` to the `ChunkedBuffer`. +-/ +@[inline] +def push (c : ChunkedBuffer) (b : ByteArray) : ChunkedBuffer := + { data := c.data.push b, size := c.size + b.size } + +/-- +Writes a `ByteArray` to the `ChunkedBuffer`. +-/ +@[inline] +def write (buffer : ChunkedBuffer) (data : ByteArray) : ChunkedBuffer := + buffer.push data + +/-- +Writes a `ChunkedBuffer` to the `ChunkedBuffer`. +-/ +@[inline] +def append (buffer : ChunkedBuffer) (data : ChunkedBuffer) : ChunkedBuffer := + { data := buffer.data ++ data.data, size := buffer.size + data.size } + +/-- +Writes a `Char` to the `ChunkedBuffer`. Only the low byte is written (`Char.toUInt8`), +so this is only correct for ASCII characters. +-/ +@[inline] +def writeChar (buffer : ChunkedBuffer) (data : Char) : ChunkedBuffer := + buffer.push (ByteArray.mk #[data.toUInt8]) + +/-- +Writes a `String` to the `ChunkedBuffer`. +-/ +@[inline] +def writeString (buffer : ChunkedBuffer) (data : String) : ChunkedBuffer := + buffer.push data.toUTF8 + +/-- +Turn the combined structure into a single contiguous ByteArray. +-/ +@[inline] +def toByteArray (cb : ChunkedBuffer) : ByteArray := + if h : 1 = cb.data.size then + cb.data[0]'(Nat.le_of_eq h) + else + cb.data.foldl (· ++ ·) (.emptyWithCapacity cb.size) + +/-- +Build from a ByteArray directly. +-/ +@[inline] +def ofByteArray (bs : ByteArray) : ChunkedBuffer := + { data := #[bs], size := bs.size } + +/-- +Build from an array of ByteArrays directly. +-/ +@[inline] +def ofArray (bs : Array ByteArray) : ChunkedBuffer := + { data := bs, size := bs.foldl (· + ·.size) 0 } + +/-- +Checks whether the buffer is empty. +-/ +@[inline] +def isEmpty (bb : ChunkedBuffer) : Bool := + bb.size = 0 + +instance : Inhabited ChunkedBuffer := ⟨empty⟩ + +instance : EmptyCollection ChunkedBuffer where + emptyCollection := empty + +instance : Coe ByteArray ChunkedBuffer where + coe := ofByteArray + +instance : Coe (Array ByteArray) ChunkedBuffer where + coe := ofArray + +end Std.Http.Internal.ChunkedBuffer diff --git a/src/Std/Internal/Http/Internal/Encode.lean b/src/Std/Internal/Http/Internal/Encode.lean new file mode 100644 index 0000000000..736091f45d --- /dev/null +++ b/src/Std/Internal/Http/Internal/Encode.lean @@ -0,0 +1,38 @@ +/- +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.Internal.ChunkedBuffer +public import Std.Internal.Http.Data.Version + +public section + +/-! +# Encode + +Serializes types to a `ChunkedBuffer` containing their canonical HTTP representation for a specific +protocol version. +-/ + +namespace Std.Http.Internal + +set_option linter.all true + +/-- +Serializes a type `t` to a `ChunkedBuffer` containing its canonical HTTP representation for protocol +version `v`. +-/ +class Encode (v : Version) (t : Type) where + /-- + Encodes a type `t` to a `ChunkedBuffer`. + -/ + encode : ChunkedBuffer → t → ChunkedBuffer + +instance : Encode .v11 Version where + encode buffer := buffer.writeString ∘ toString + +end Std.Http.Internal diff --git a/src/Std/Internal/Http/Internal/String.lean b/src/Std/Internal/Http/Internal/String.lean new file mode 100644 index 0000000000..2939df6a22 --- /dev/null +++ b/src/Std/Internal/Http/Internal/String.lean @@ -0,0 +1,117 @@ +/- +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 +import Init.Grind +public import Init.Data.String +public import Std.Internal.Http.Internal.Char + +public section + + +/-! +# Internal String Helpers + +Shared string utilities for HTTP: token validation and quoted-string encoding/decoding for header +parameter values and chunk extensions. +-/ + +namespace Std.Http.Internal + +open Char + +set_option linter.all true + +/-- +Core character quoting used by `String.quote`. + +In string context (`inString := true`), this emits: +- `qdtext` characters directly +- `"` and `\\` as `quoted-pair` +and panics for characters outside the grammar. +-/ +def quoteCore (c : Char) (inString : Bool := false) : String := + if inString then + if qdtext c then + .singleton c + else if c = '\\' || c = '\"' then + .append "\\" (.singleton c) + else + panic! "invalid HTTP quoted-string content" + else + if quotedPairChar c then + .singleton c + else + panic! "invalid HTTP quoted-pair content" + +/-- +Attempts to quote `s` as an HTTP `quoted-string`: +`DQUOTE *( qdtext / quoted-pair ) DQUOTE`. + +Returns `none` when any character in `s` cannot be represented by the grammar. +-/ +@[expose] +def quoteHttpString? (s : String) : Option String := + if s.all tchar ∧ ¬s.isEmpty then + some s + else if s.all quotedStringChar then + some (.append + (.foldl (fun acc c => + .append acc (quoteCore c (inString := true))) "\"" s) + "\"") + else + none + +/-- +Quotes `s` as an HTTP `quoted-string`, panicking if `s` contains characters that cannot be +represented by `qdtext`/`quoted-pair`. +-/ +def quoteHttpString! (s : String) : String := + match quoteHttpString? s with + | some res => res + | none => panic! "invalid HTTP quoted-string content" + +private inductive UnquoteState where + | start + | valid (escaped : Bool) (acc : String) + | done (result : String) + | invalid + +/-- +Parses an HTTP `quoted-string`, returning the unescaped content when valid. +-/ +def unquoteHttpString? (s : String) : Option String := + if s.startsWith '"' then + match s.foldl (fun (st : UnquoteState) c => + match st with + | .start => + if c == '"' then .valid false "" else .invalid + | .valid false acc => + if c == '\\' then .valid true acc + else if c == '"' then .done acc + else if qdtext c then .valid false (acc.push c) + else .invalid + | .valid true acc => + if quotedPairChar c then .valid false (acc.push c) + else .invalid + | .done _ | .invalid => .invalid) .start with + | .done result => some result + | _ => none + else if s.all Char.tchar then + some s + else + none + +/-- +Checks whether a string is a valid non-empty HTTP token. +-/ +@[expose] +def isToken (s : String) : Bool := + let s := s.toList + ¬s.isEmpty ∧ s.all Char.tchar + +end Std.Http.Internal diff --git a/tests/lean/run/async_http_encode.lean b/tests/lean/run/async_http_encode.lean new file mode 100644 index 0000000000..a46473409e --- /dev/null +++ b/tests/lean/run/async_http_encode.lean @@ -0,0 +1,504 @@ +import Std.Internal.Http.Data.Chunk +import Std.Internal.Http.Data.Request +import Std.Internal.Http.Data.Response + +open Std.Http +open Std.Http.Internal + +private def encodeStr [Encode .v11 t] (v : t) : String := + String.fromUTF8! (Encode.encode (v := .v11) ChunkedBuffer.empty v).toByteArray + +/-! ## Version encoding -/ + +/-- +info: "HTTP/1.1" +-/ +#guard_msgs in +#eval encodeStr Version.v11 + +/-- +info: "HTTP/2.0" +-/ +#guard_msgs in +#eval encodeStr Version.v20 + +/-- +info: "HTTP/3.0" +-/ +#guard_msgs in +#eval encodeStr Version.v30 + +/-! ## Method encoding -/ + +/-- +info: "GET" +-/ +#guard_msgs in +#eval encodeStr Method.get + +/-- +info: "HEAD" +-/ +#guard_msgs in +#eval encodeStr Method.head + +/-- +info: "POST" +-/ +#guard_msgs in +#eval encodeStr Method.post + +/-- +info: "PUT" +-/ +#guard_msgs in +#eval encodeStr Method.put + +/-- +info: "DELETE" +-/ +#guard_msgs in +#eval encodeStr Method.delete + +/-- +info: "CONNECT" +-/ +#guard_msgs in +#eval encodeStr Method.connect + +/-- +info: "OPTIONS" +-/ +#guard_msgs in +#eval encodeStr Method.options + +/-- +info: "TRACE" +-/ +#guard_msgs in +#eval encodeStr Method.trace + +/-- +info: "PATCH" +-/ +#guard_msgs in +#eval encodeStr Method.patch + +/-! ## Status encoding -/ + +/-- +info: "200 OK" +-/ +#guard_msgs in +#eval encodeStr Status.ok + +/-- +info: "201 Created" +-/ +#guard_msgs in +#eval encodeStr Status.created + +/-- +info: "404 Not Found" +-/ +#guard_msgs in +#eval encodeStr Status.notFound + +/-- +info: "500 Internal Server Error" +-/ +#guard_msgs in +#eval encodeStr Status.internalServerError + +/-- +info: "999 Unknown" +-/ +#guard_msgs in +#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩) + +/-! ## Request.line encoding -/ + +/-- +info: "GET /path HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "/path" } : Request.Head) + +/-- +info: "POST /submit HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .post, version := .v11, uri := "/submit" } : Request.Head) + +/-- +info: "PUT /resource HTTP/2.0\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ + method := .put + version := .v20 + uri := "/resource" + } : Request.Head) + +/-! ## Response.line encoding -/ + +/-- +info: "HTTP/1.1 200 OK\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .ok, version := .v11 } : Response.Head) + +/-- +info: "HTTP/1.1 404 Not Found\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .notFound, version := .v11 } : Response.Head) + +/-- +info: "HTTP/2.0 500 Internal Server Error\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ + status := .internalServerError + version := .v20 + } : Response.Head) + +/-! ## Chunk encoding -/ + +/-- +info: "5\x0d\nhello\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "hello".toUTF8) + +/-- +info: "0\x0d\n\x0d\n" +-/ +#guard_msgs in +#eval encodeStr Chunk.empty + +/-- +info: "3;lang=en\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "lang") (.ofString! "en")) + +/-- +info: "3;lang=\"en \\\" u\";type=text\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "lang") (.ofString! "en \" u") |>.insertExtension (Chunk.ExtensionName.mk "type") (.ofString! "text")) + +/-- +info: "a\x0d\n0123456789\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "0123456789".toUTF8) + +/-! ## Request builder -/ + +/-- +info: "GET /index.html HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.get "/index.html" |>.body ()).line + +/-- +info: "POST /api/data HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.post "/api/data" |>.body ()).line + +/-- +info: "PUT /resource HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.put "/resource" |>.body ()).line + +/-- +info: "DELETE /item HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.delete "/item" |>.body ()).line + +/-- +info: "PATCH /update HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.patch "/update" |>.body ()).line + +/-- +info: "HEAD /check HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.head "/check" |>.body ()).line + +/-- +info: "OPTIONS * HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.options "*" |>.body ()).line + +/-- +info: "CONNECT proxy:8080 HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.connect "proxy:8080" |>.body ()).line + +/-- +info: "TRACE /debug HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.trace "/debug" |>.body ()).line + +/-- +info: "POST /v2 HTTP/2.0\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Request.new |>.method .post |>.uri "/v2" |>.version .v20 |>.body ()).line + +/-! ## Response builder -/ + +/-- +info: "HTTP/1.1 200 OK\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.ok |>.body ()).line + +/-- +info: "HTTP/1.1 404 Not Found\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.notFound |>.body ()).line + +/-- +info: "HTTP/1.1 500 Internal Server Error\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.internalServerError |>.body ()).line + +/-- +info: "HTTP/1.1 400 Bad Request\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.badRequest |>.body ()).line + +/-- +info: "HTTP/1.1 201 Created\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.created |>.body ()).line + +/-- +info: "HTTP/1.1 202 Accepted\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.accepted |>.body ()).line + +/-- +info: "HTTP/1.1 401 Unauthorized\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.unauthorized |>.body ()).line + +/-- +info: "HTTP/1.1 403 Forbidden\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.forbidden |>.body ()).line + +/-- +info: "HTTP/1.1 409 Conflict\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.conflict |>.body ()).line + +/-- +info: "HTTP/1.1 503 Service Unavailable\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.serviceUnavailable |>.body ()).line + +/-- +info: "HTTP/1.1 418 I'm a teapot\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Response.withStatus .imATeapot |>.body ()).line + +/-! ## Edge cases: Status encoding -/ + +-- Status.other 0: minimum possible value +/-- +info: "999 Unknown" +-/ +#guard_msgs in +#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩) + +-- Status.other that overlaps with a named status (100 = Continue) +/-- +info: "888 Unknown" +-/ +#guard_msgs in +#eval encodeStr (Status.other ⟨888, "Unknown", by decide, by decide, by decide⟩) + +-- Status.other max UInt16 +/-- +info: "999 Unknown" +-/ +#guard_msgs in +#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩) + +-- Non-standard status code in the middle +/-- +info: "299 Unknown" +-/ +#guard_msgs in +#eval encodeStr (Status.other ⟨299, "Unknown", by decide, by decide, by decide⟩) + +/-! ## Edge cases: Chunk size hex encoding -/ + +-- Size 16 → hex "10" (first two-digit hex) +/-- +info: "10\x0d\n0123456789abcdef\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "0123456789abcdef".toUTF8) + +-- Size 255 → hex "ff": verify prefix +/-- +info: true +-/ +#guard_msgs in +#eval do + let data := ByteArray.mk (Array.replicate 255 (0x41 : UInt8)) + return encodeStr (Chunk.ofByteArray data) |>.startsWith "ff\r\n" + +-- Size 256 → hex "100" (first three-digit hex): verify prefix +/-- +info: true +-/ +#guard_msgs in +#eval do + let data := ByteArray.mk (Array.replicate 256 (0x41 : UInt8)) + return encodeStr (Chunk.ofByteArray data) |>.startsWith "100\r\n" + +-- Size 15 → hex "f" (largest single hex digit) +/-- +info: "f\x0d\n0123456789abcde\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "0123456789abcde".toUTF8) + +-- Chunk.ofByteArray with empty data (same as Chunk.empty) +/-- +info: "0\x0d\n\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray ByteArray.empty) + +/-! ## Edge cases: Chunk extensions -/ + +-- Extension with no value (None case) via direct struct construction +/-- +info: "3;marker\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ data := "abc".toUTF8, extensions := #[(Chunk.ExtensionName.mk "marker", none)] } : Chunk) + +-- Extension with empty string value (not quoted since "".any returns false) +/-- +info: "3;key=\"\"\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "")) + +-- Extension value that is all token chars (no quoting needed) +/-- +info: "3;key=abc123\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "abc123")) + +-- Extension value with space (must be quoted) +/-- +info: "3;key=\"hello world\"\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "hello world")) + +-- Extension value with backslash (must be escaped) +/-- +info: "3;key=\"a\\\\b\"\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "a\\b")) + +-- Multiple extensions with no value and with value +/-- +info: "3;a;b=1\x0d\nabc\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ data := "abc".toUTF8, extensions := #[(Chunk.ExtensionName.mk "a", none), (Chunk.ExtensionName.mk "b", some (.ofString! "1"))] } : Chunk) + +/-! ## Edge cases: Request URI encoding -/ + +-- URI with query parameters +/-- +info: "GET /search?q=hello&lang=en HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "/search?q=hello&lang=en" } : Request.Head) + +-- URI with fragment +/-- +info: "GET /page#section HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "/page#section" } : Request.Head) + +-- URI with percent-encoded characters +/-- +info: "GET /path%20with%20spaces HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "/path%20with%20spaces" } : Request.Head) + +-- URI with special characters (brackets, colons) +/-- +info: "GET /api/v1/users/[id]:action HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "/api/v1/users/[id]:action" } : Request.Head) + +-- Empty URI +/-- +info: "GET HTTP/1.1\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ method := .get, version := .v11, uri := "" } : Request.Head) + +/-! ## Edge cases: Response with unusual statuses -/ + +/-- +info: "HTTP/1.1 100 Continue\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .«continue», version := .v11 } : Response.Head) + +/-- +info: "HTTP/1.1 204 No Content\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .noContent, version := .v11 } : Response.Head) + +/-- +info: "HTTP/1.1 301 Moved Permanently\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .movedPermanently, version := .v11 } : Response.Head) + +/-- +info: "HTTP/3.0 200 OK\x0d\n" +-/ +#guard_msgs in +#eval encodeStr ({ status := .ok, version := .v30 } : Response.Head) diff --git a/tests/lean/run/async_http_string_quoting.lean b/tests/lean/run/async_http_string_quoting.lean new file mode 100644 index 0000000000..7b19eb3bfb --- /dev/null +++ b/tests/lean/run/async_http_string_quoting.lean @@ -0,0 +1,85 @@ +import Std.Internal.Http.Internal.String +import Std.Internal.Http.Internal.Char + +open Std.Http.Internal + +private def c (n : Nat) : Char := Char.ofNat n + +#guard Std.Http.Internal.Char.qdtext (c 0x08) = false +#guard Std.Http.Internal.Char.qdtext (c 0x09) = true +#guard Std.Http.Internal.Char.qdtext (c 0x0a) = false +#guard Std.Http.Internal.Char.qdtext (c 0x1f) = false +#guard Std.Http.Internal.Char.qdtext (c 0x20) = true +#guard Std.Http.Internal.Char.qdtext (c 0x21) = true +#guard Std.Http.Internal.Char.qdtext (c 0x22) = false +#guard Std.Http.Internal.Char.qdtext (c 0x23) = true +#guard Std.Http.Internal.Char.qdtext (c 0x5b) = true +#guard Std.Http.Internal.Char.qdtext (c 0x5c) = false +#guard Std.Http.Internal.Char.qdtext (c 0x5d) = true +#guard Std.Http.Internal.Char.qdtext (c 0x7e) = true +#guard Std.Http.Internal.Char.qdtext (c 0x7f) = false + +#guard Std.Http.Internal.Char.quotedPairChar (c 0x08) = false +#guard Std.Http.Internal.Char.quotedPairChar (c 0x09) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x1f) = false +#guard Std.Http.Internal.Char.quotedPairChar (c 0x20) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x21) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x22) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x5c) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x7e) = true +#guard Std.Http.Internal.Char.quotedPairChar (c 0x7f) = false + +#guard Std.Http.Internal.Char.quotedStringChar (c 0x09) = true +#guard Std.Http.Internal.Char.quotedStringChar (c 0x20) = true +#guard Std.Http.Internal.Char.quotedStringChar (c 0x22) = true +#guard Std.Http.Internal.Char.quotedStringChar (c 0x5c) = true +#guard Std.Http.Internal.Char.quotedStringChar (c 0x0a) = false +#guard Std.Http.Internal.Char.quotedStringChar (c 0x0d) = false +#guard Std.Http.Internal.Char.quotedStringChar (c 0x7f) = false + +#guard quoteHttpString? "token" = some "token" +#guard quoteHttpString? "a\t " = some "\"a\t \"" +#guard quoteHttpString? "atabpo\n\t " = none +#guard quoteHttpString? "" = some "\"\"" +#guard quoteHttpString? "\"" = some "\"\\\"\"" +#guard quoteHttpString? "\\" = some "\"\\\\\"" +#guard quoteHttpString? "\"\\\"" = some "\"\\\"\\\\\\\"\"" +#guard quoteHttpString? "abc\rdef" = none +#guard quoteHttpString? "abc\ndef" = none +#guard quoteHttpString? "abc\u0000def" = none + +#guard unquoteHttpString? "\"token\"" = some "token" +#guard unquoteHttpString? "\"a\\\\\\\"b\"" = some "a\\\"b" +#guard unquoteHttpString? "\"line1\nline2\"" = none +#guard unquoteHttpString? "\"\"" = some "" +#guard unquoteHttpString? "\"\\\\\"" = some "\\" +#guard unquoteHttpString? "\"\\\"\"" = some "\"" +#guard unquoteHttpString? "\"a\\tb\"" = some "atb" +#guard unquoteHttpString? "\"a\tb\"" = some "a\tb" +#guard unquoteHttpString? "token" = some "token" +#guard unquoteHttpString? "\"" = none +#guard unquoteHttpString? "\"abc" = none +#guard unquoteHttpString? "\"abc\\\"" = none +#guard unquoteHttpString? "\"abc\\\n\"" = none +#guard unquoteHttpString? "\"abc\r\"" = none + +private def isQuotedString (s : String) : Bool := + s.startsWith '"' && (unquoteHttpString? s).isSome + +#guard isQuotedString "\"abc\"" = true +#guard isQuotedString "\"ab\\\\\\\"c\"" = true +#guard isQuotedString "\"ab\nc\"" = false +#guard isQuotedString "\"\"" = true +#guard isQuotedString "\"\\\"\"" = true +#guard isQuotedString "\"\\\\\"" = true +#guard isQuotedString "abc" = false +#guard isQuotedString "\"" = false +#guard isQuotedString "\"abc" = false +#guard isQuotedString "\"abc\\\"" = false + +#guard unquoteHttpString? (quoteHttpString! "abc\t ") = some "abc\t " +#guard unquoteHttpString? (quoteHttpString! "a\\\"b") = some "a\\\"b" +#guard unquoteHttpString? (quoteHttpString! "") = some "" +#guard unquoteHttpString? (quoteHttpString! "\"") = some "\"" +#guard unquoteHttpString? (quoteHttpString! "\\") = some "\\" +#guard unquoteHttpString? (quoteHttpString! " !#$%&'()*+,-./:;<=>?@[\\]^_`{|}~") = some " !#$%&'()*+,-./:;<=>?@[\\]^_`{|}~"