sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'sofia/async-http-headers' into sofia/async-http-uri

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 12:12:38 -03:00
parent 67822f4c42 6189d4c130
commit 203d5362d4
9 changed files with 125 additions and 336 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Std/Internal/Http/Data/Chunk.lean
View File

@@ -51,7 +51,7 @@ structure ExtensionName where
/--
The proof that it's a valid extension name.
-/
validExtensionName : IsValidExtensionName value := by decide
isValidExtensionName : IsValidExtensionName value := by decide
deriving Repr, DecidableEq, BEq
instance : Hashable ExtensionName where

13
src/Std/Internal/Http/Data/Extensions.lean
View File

@@ -30,17 +30,6 @@ set_option linter.all true
`quickCmp` is unavailable here, so this is a simpler implementation of the same comparison.
-/
private def compareString (s₁ s₂ : String) : Ordering :=
let rec go : List Char → List Char → Ordering
| [], [] => .eq
| [], _ => .lt
| _, [] => .gt
| c₁ :: cs₁, c₂ :: cs₂ =>
match compare c₁.toNat c₂.toNat with
| .eq => go cs₁ cs₂
| ord => ord
go s₁.toList s₂.toList
/--
An ordering for `Name` keys used by `Extensions`.
-/
@@ -50,7 +39,7 @@ protected def Extensions.compareName : Name → Name → Ordering
| _, .anonymous => .gt
| .str p₁ s₁, .str p₂ s₂ =>
match Extensions.compareName p₁ p₂ with
| .eq => compareString s₁ s₂
| .eq => compareOfLessAndEq s₁ s₂
| ord => ord
| .str _ _, .num _ _ => .lt
| .num _ _, .str _ _ => .gt

27
src/Std/Internal/Http/Data/Request.lean
View File

@@ -66,7 +66,7 @@ structure Request (t : Type) where
/--
The request line information (`method`, `version`, and request-target `uri`).
-/
head : Request.Head
line : Request.Head
/--
The request body content of type t.
@@ -84,9 +84,9 @@ Builds an HTTP Request.
-/
structure Request.Builder where
/--
The head of the request.
The request-line of an HTTP request.
-/
head : Head := { method := .get, version := .v11, uri := .asteriskForm }
line : Head := { method := .get, version := .v11, uri := .asteriskForm }
/--
Optional dynamic metadata attached to the request.
@@ -134,38 +134,38 @@ 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 } }
{ 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 head := { builder.head with version := version } }
{ builder with line := { builder.line 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 } }
{ builder with line := { builder.line with uri := uri } }
/--
Sets the request target/URI for the request being built
-/
def uri! (builder : Builder) (uri : String) : Builder :=
let uri := RequestTarget.parse! uri
{ builder with head := { builder.head with uri } }
{ builder with line := { builder.line with uri } }
/--
Sets the headers for the request being built
-/
def headers (builder : Builder) (headers : Headers) : Builder :=
{ builder with head := { builder.head with headers } }
{ builder with line := { builder.line with headers } }
/--
Adds a single header to the request being built.
-/
def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the request being built, panics if the header is invalid.
@@ -173,7 +173,7 @@ Adds a single header to the request being built, panics if the header is invalid
def header! (builder : Builder) (key : String) (value : String) : Builder :=
let key := Header.Name.ofString! key
let value := Header.Value.ofString! value
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the request being built.
@@ -182,7 +182,7 @@ Returns `none` if the header name or value is invalid.
def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
let key ← Header.Name.ofString? key
let value ← Header.Value.ofString? value
pure <| { builder with head := { builder.head with headers := builder.head.headers.insert key value } }
pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a header to the request being built only if the Option Header.Value is some.
@@ -202,7 +202,7 @@ def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
Builds and returns the final HTTP Request with the specified body.
-/
def body (builder : Builder) (body : t) : Request t :=
{ head := builder.head, body := body, extensions := builder.extensions }
{ line := builder.line, body := body, extensions := builder.extensions }
end Builder
@@ -248,9 +248,8 @@ def patch (uri : RequestTarget) : Builder :=
/--
Creates a new HTTP HEAD Request builder with the specified URI.
Named `head'` to avoid conflict with the `head` field accessor.
-/
def head' (uri : RequestTarget) : Builder :=
def head (uri : RequestTarget) : Builder :=
new
|>.method .head
|>.uri uri

20
src/Std/Internal/Http/Data/Response.lean
View File

@@ -52,7 +52,7 @@ structure Response (t : Type) where
/--
The response status-line information.
-/
head : Response.Head := {}
line : Response.Head := {}
/--
The content of the response.
@@ -70,9 +70,9 @@ Builds an HTTP Response.
-/
structure Response.Builder where
/--
The response status-line information.
The start-line of an HTTP request (method, request-target, and version).
-/
head : Head := {}
line : Head := {}
/--
Optional dynamic metadata attached to the response.
@@ -117,19 +117,19 @@ 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 } }
{ builder with line := { builder.line with status := status } }
/--
Sets the headers for the response being built.
-/
def headers (builder : Builder) (headers : Headers) : Builder :=
{ builder with head := { builder.head with headers } }
{ builder with line := { builder.line with headers } }
/--
Adds a single header to the response being built.
-/
def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the response being built, panics if the header is invalid.
@@ -137,7 +137,7 @@ Adds a single header to the response being built, panics if the header is invali
def header! (builder : Builder) (key : String) (value : String) : Builder :=
let key := Header.Name.ofString! key
let value := Header.Value.ofString! value
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the response being built.
@@ -146,7 +146,7 @@ Returns `none` if the header name or value is invalid.
def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
let key ← Header.Name.ofString? key
let value ← Header.Value.ofString? value
pure <| { builder with head := { builder.head with headers := builder.head.headers.insert key value } }
pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Inserts a typed extension value into the response being built.
@@ -158,14 +158,14 @@ def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
Builds and returns the final HTTP Response with the specified body.
-/
def body (builder : Builder) (body : t) : Response t :=
{ head := builder.head, body := body, extensions := builder.extensions }
{ 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 :=
{ head := builder.head, body := {}, extensions := builder.extensions }
{ line := builder.line, body := {}, extensions := builder.extensions }
end Builder

7
src/Std/Internal/Http/Data/Status.lean
View File

@@ -39,15 +39,14 @@ abbrev IsValidReasonPhrase (s : String) : Prop :=
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 : UInt16 → Bool
| 100 | 101 | 102 | 103
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 => true
| _ => false
| 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

9
src/Std/Internal/Http/Data/Version.lean
View File

@@ -29,6 +29,11 @@ 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`
-/
@@ -51,6 +56,7 @@ 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
@@ -60,6 +66,7 @@ def ofNumber? : Nat → Nat → Option Version
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
@@ -77,12 +84,14 @@ def ofString! (s : String) : Version :=
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"

331
src/Std/Internal/Http/Internal/Char.lean
View File

@@ -26,7 +26,7 @@ set_option linter.all true
/--
Checks if a character is ASCII (Unicode code point < 128).
-/
@[expose]
@[inline, expose]
def isAscii (c : Char) : Bool :=
c.toNat < 128
@@ -47,7 +47,7 @@ def isAlphaChar (c : Char) : Bool :=
/--
Checks if a byte represents an ASCII character (value < 128).
-/
@[expose]
@[inline, expose]
def isAsciiByte (c : UInt8) : Bool :=
c < 128
@@ -65,195 +65,113 @@ Checks if a byte is an alphabetic character (a-z or A-Z).
def isAlpha (c : UInt8) : Bool :=
(c >= 'A'.toUInt8 && c <= 'Z'.toUInt8) || (c >= 'a'.toUInt8 && c <= 'z'.toUInt8)
/--
Two character predicates are equivalent on ASCII input (`0x00`-`0x7F`).
-/
abbrev EqOnAscii (x : Char → Bool) (y : Char → Bool) : Prop :=
∀ n < 128, x (Char.ofNat n) ↔ y (Char.ofNat n)
/--
tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
/ "+" / "-" / "." / "^" / "_" / "`" / "|" / "~"
/ DIGIT / ALPHA
; Visible token characters used to build `token`.
-/
@[inline]
def tchar (c : Char) : Bool :=
"!#$%&'*+-.^_`|~".toList.contains c
∨ isDigitChar c
∨ isAlphaChar c
/--
Checks if a character is a valid HTTP token character per RFC 9110 §5.6.2.
token = 1*tchar
-/
def token (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x57ffffffc7fffffe03ff6cfa00000000 c.toNat
theorem token_eq_tchar_on_ascii : EqOnAscii token tchar := by
decide
(c matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' | '+' | '-' | '.' | '^' | '_' | '`' | '|' | '~') ||
isDigitChar c ||
isAlphaChar c
/--
vchar = %x21-7E
; Visible (printing) ASCII characters.
-/
def vcharSpec (c : Char) : Bool :=
c ≥ '!' ∧ c ≤ '~'
/--
Checks if `c` is a visible (printing) ASCII character.
-/
@[inline]
def vchar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
theorem vchar_eq_vcharSpec_on_ascii : EqOnAscii vchar vcharSpec := by
decide
c ≥ '!' ∧ c ≤ '~'
/--
qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E
; ASCII-only variant (no obs-text).
-/
def qdtextSpec (c : Char) : Bool :=
c = '\t' ∨
c = ' ' ∨
c = '!' ∨
('#' ≤ c ∧ c ≤ '[') ∨
@[inline]
def qdtext (c : Char) : Bool :=
(c matches '\t' | ' ' | '!') ||
('#' ≤ c ∧ c ≤ '[') ||
(']' ≤ c ∧ c ≤ '~')
/--
Checks if `c` is valid `qdtext` in an HTTP `quoted-string` (ASCII-only).
-/
def qdtext (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffeffffffffffffffb00000200 c.toNat
theorem qdtext_eq_qdtextSpec_on_ascii : EqOnAscii qdtext qdtextSpec := by
decide
/--
quoted-pair = "\" ( HTAB / SP / VCHAR )
quoted-pair = "\\" ( HTAB / SP / VCHAR )
; ASCII-only variant (no obs-text).
-/
def quotedPairCharSpec (c : Char) : Bool :=
c = '\t' ∨ c = ' ' ∨ vchar c
/--
Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
-/
@[inline]
def quotedPairChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem quotedPairChar_eq_quotedPairCharSpec_on_ascii :
EqOnAscii quotedPairChar quotedPairCharSpec := by
decide
(c matches '\t' | ' ') || vchar c
/--
quoted-string body character class:
( qdtext / quoted-pair payload ) in ASCII-only mode.
-/
def quotedStringCharSpec (c : Char) : Bool :=
qdtext c ∨ quotedPairChar c
/--
Returns `true` when `c` can be represented inside an HTTP `quoted-string` body:
either directly as `qdtext` or via `quoted-pair`.
-/
@[inline]
def quotedStringChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem quotedStringChar_eq_quotedStringCharSpec_on_ascii :
EqOnAscii quotedStringChar quotedStringCharSpec := by
decide
qdtext c || quotedPairChar c
/--
field-vchar = VCHAR
; ASCII-only variant (no obs-text).
-/
def fieldVcharSpec (c : Char) : Bool :=
vchar c
/--
Checks if `c` is valid `field-vchar` in ASCII-only mode.
-/
@[inline]
def fieldVchar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
theorem fieldVchar_eq_fieldVcharSpec_on_ascii : EqOnAscii fieldVchar fieldVcharSpec := by
decide
vchar c
/--
field-content character class:
field-vchar / SP / HTAB
; ASCII-only variant (no obs-text).
-/
def fieldContentSpec (c : Char) : Bool :=
fieldVchar c ∨ c = ' ' ∨ c = '\t'
/--
Checks if `c` is valid in the body of an HTTP `field-content` (ASCII-only).
-/
@[inline]
def fieldContent (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem fieldContent_eq_fieldContentSpec_on_ascii : EqOnAscii fieldContent fieldContentSpec := by
decide
fieldVchar c || (c matches ' ' | '\t')
/--
ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E
; ASCII-only variant (no obs-text).
-/
def ctextSpec (c : Char) : Bool :=
c = '\t' ∨
c = ' ' ∨
('!' ≤ c ∧ c ≤ '\'') ∨
('*' ≤ c ∧ c ≤ '[') ∨
(']' ≤ c ∧ c ≤ '~')
/--
Checks if `c` is valid `ctext` in an HTTP comment (ASCII-only).
-/
@[inline]
def ctext (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffeffffffffffffcff00000200 c.toNat
theorem ctext_eq_ctextSpec_on_ascii : EqOnAscii ctext ctextSpec := by
decide
(c matches '\t' | ' ') ||
('!' ≤ c ∧ c ≤ '\'') ||
('*' ≤ c ∧ c ≤ '[') ||
(']' ≤ c ∧ c ≤ '~')
/--
etagc = "!" / %x23-7E
; ASCII-only variant (no obs-text).
-/
def etagcSpec (c : Char) : Bool :=
c = '!' ∨ ('#' ≤ c ∧ c ≤ '~')
/--
Checks if `c` is valid `etagc` inside an `opaque-tag` (ASCII-only).
-/
@[inline]
def etagc (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffa00000000 c.toNat
theorem etagc_eq_etagcSpec_on_ascii : EqOnAscii etagc etagcSpec := by
decide
c = '!' || ('#' ≤ c ∧ c ≤ '~')
/--
OWS = *( SP / HTAB ) (character class only)
-/
@[inline]
def ows (c : Char) : Bool :=
c = ' ' ∨ c = '\t'
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
@@ -264,40 +182,22 @@ HTAB / SP / VCHAR
Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
-/
def reasonPhraseCharSpec (c : Char) : Bool :=
c = '\t' ∨ c = ' ' ∨ vchar c
/--
Checks if `c` is valid inside an HTTP `reason-phrase` per RFC 9110 §15.
-/
@[inline]
def reasonPhraseChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem reasonPhraseChar_eq_reasonPhraseCharSpec : EqOnAscii reasonPhraseChar reasonPhraseCharSpec := by
decide
(c matches '\t' | ' ') || vchar c
/--
Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F) using a precomputed bitmask.
Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
-/
def isHexDigitSpec (c : Char) : Bool :=
(c ≥ '0' && c ≤ '9') ||
(c ≥ 'a' && c ≤ 'f') ||
(c ≥ 'A' && c ≤ 'F')
/--
Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F) using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isHexDigit (c : Char) : Bool :=
Nat.testBit 0x0000007e0000007e03ff000000000000 c.toNat
theorem isHexDigit_eq_isHexDigitSpec_on_ascii : EqOnAscii isHexDigit isHexDigitSpec := by
decide
(c matches 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') ||
isDigitChar c
/--
Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
-/
@[expose]
@[inline, expose]
def isHexDigitByte (c : UInt8) : Bool :=
(c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
(c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) ||
@@ -306,118 +206,54 @@ def isHexDigitByte (c : UInt8) : Bool :=
/--
Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
-/
def isAlphaNumSpec (c : UInt8) : Bool :=
@[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 if a byte is an alphanumeric digit (0-9, a-z, or A-Z) using a precomputed bitmask.
-/
@[expose]
def isAlphaNum (c : UInt8) : Bool :=
Nat.testBit 0x7fffffe07fffffe03ff000000000000 c.toNat
theorem isAlphaNum_eq_isAlphaNumSpec_on_ascii :
∀ i : Fin 128, isAlphaNum (UInt8.ofNat i.1) = isAlphaNumSpec (UInt8.ofNat i.1) := by
decide
/--
Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
Checks whether `c` is an ASCII alphanumeric character.
-/
@[inline, expose]
def isAsciiAlphaNumCharSpec (c : Char) : Bool :=
isAscii c && isAlphaNum (UInt8.ofNat c.toNat)
/--
Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
-/
def isAsciiAlphaNumChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff000000000000 c.toNat
theorem isAsciiAlphaNumChar_eq_isAsciiAlphaNumCharSpec_on_ascii :
EqOnAscii isAsciiAlphaNumChar isAsciiAlphaNumCharSpec := by
decide
/--
Checks if a character is valid after the first character of a URI scheme.
Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
-/
@[expose]
def isValidSchemeCharSpec (c : Char) : Bool :=
isAsciiAlphaNumCharSpec c || c == '+' || c == '-' || c == '.'
isAscii c && (isDigitChar c || isAlphaChar 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 :=
isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff680000000000 c.toNat
theorem isValidSchemeCharChar_eq_isValidSchemeCharCharSpec_on_ascii :
EqOnAscii isValidSchemeChar isValidSchemeCharSpec := by
decide
isAsciiAlphaNumChar c || (c matches '+' | '-' | '.')
/--
Checks if a character is valid for use in a domain name.
Valid characters are ASCII alphanumeric, hyphens, and dots.
-/
@[expose]
def isValidDomainNameCharSpec (c : Char) : Bool :=
isAsciiAlphaNumCharSpec c || c == '-' || c == '.'
/--
Checks if a character is valid for use in a domain name.
-/
@[inline, expose]
def isValidDomainNameChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff600000000000 c.toNat
theorem isValidDomainNameChar_eq_isValidDomainNameCharSpec_on_ascii :
EqOnAscii isValidDomainNameChar isValidDomainNameCharSpec := by
decide
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.
-/
def isUnreservedSpec (c : UInt8) : Bool :=
isAlphaNumSpec c ||
(c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8)
/--
Checks if a byte is an unreserved character according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isUnreserved (c : UInt8) : Bool :=
Nat.testBit 0x47fffffe87fffffe03ff600000000000 c.toNat
theorem isUnreserved_eq_isUnreservedSpec_on_ascii :
∀ i : Fin 128, isUnreserved (UInt8.ofNat i.1) = isUnreservedSpec (UInt8.ofNat i.1) := by
decide
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: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`.
-/
def isSubDelimsSpec (c : UInt8) : Bool :=
c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = '\''.toUInt8 ||
@[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 sub-delimiter character according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
def isSubDelims (c : UInt8) : Bool :=
Nat.testBit 0x28001fd200000000 c.toNat
theorem isSubDelims_eq_isSubDelimsSpec_on_ascii :
∀ i : Fin 128, isSubDelims (UInt8.ofNat i.1) = isSubDelimsSpec (UInt8.ofNat i.1) := by
decide
/--
Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
`pchar = unreserved / pct-encoded / sub-delims / ":" / "@"`
@@ -425,57 +261,25 @@ Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`,
so this predicate only covers the non-percent characters.
-/
def isPCharSpec (c : UInt8) : Bool :=
isUnreservedSpec c || isSubDelimsSpec c || c = ':'.toUInt8 || c = '@'.toUInt8
/--
Checks if a byte is a valid path character (`pchar`) according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isPChar (c : UInt8) : Bool :=
Nat.testBit 0x47fffffe87ffffff2fff7fd200000000 c.toNat
theorem isPChar_eq_isPCharSpec_on_ascii :
∀ i : Fin 128, isPChar (UInt8.ofNat i.1) = isPCharSpec (UInt8.ofNat i.1) := by
decide
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 / "/" / "?" )`
-/
def isQueryCharSpec (c : UInt8) : Bool :=
isPCharSpec c || c = '/'.toUInt8 || c = '?'.toUInt8
/--
Checks if a byte is a valid character in a URI query component according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isQueryChar (c : UInt8) : Bool :=
Nat.testBit 0x47fffffe87ffffffafffffd200000000 c.toNat
theorem isQueryChar_eq_isQueryCharSpec_on_ascii :
∀ i : Fin 128, isQueryChar (UInt8.ofNat i.1) = isQueryCharSpec (UInt8.ofNat i.1) := by
decide
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 / "/" / "?" )`
-/
def isFragmentCharSpec (c : UInt8) : Bool :=
isPCharSpec c || c = '/'.toUInt8 || c = '?'.toUInt8
/--
Checks if a byte is a valid character in a URI fragment component according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isFragmentChar (c : UInt8) : Bool :=
Nat.testBit 0x47fffffe87ffffffafffffd200000000 c.toNat
theorem isFragmentChar_eq_isFragmentCharSpec_on_ascii :
∀ i : Fin 128, isFragmentChar (UInt8.ofNat i.1) = isFragmentCharSpec (UInt8.ofNat i.1) := by
decide
isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
/--
Checks if a byte is a valid character in a URI userinfo component according to RFC 3986.
@@ -484,19 +288,8 @@ Checks if a byte is a valid character in a URI userinfo component according to R
Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean`
that provides it.
-/
def isUserInfoCharSpec (c : UInt8) : Bool :=
isUnreservedSpec c || isSubDelimsSpec c || c = ':'.toUInt8
/--
Checks if a byte is a valid character in a URI userinfo component according to RFC 3986 using a precomputed bitmask.
-/
@[expose]
@[inline, expose]
def isUserInfoChar (c : UInt8) : Bool :=
Nat.testBit 0x47fffffe87fffffe2fff7fd200000000 c.toNat
theorem isUserInfoChar_eq_isUserInfoCharSpec_on_ascii :
∀ i : Fin 128, isUserInfoChar (UInt8.ofNat i.1) = isUserInfoCharSpec (UInt8.ofNat i.1) := by
decide
isUnreserved c || isSubDelims c || c = ':'.toUInt8
end Std.Http.Internal.Char

6
src/Std/Internal/Http/Internal/String.lean
View File

@@ -56,7 +56,7 @@ Returns `none` when any character in `s` cannot be represented by the grammar.
-/
@[expose]
def quoteHttpString? (s : String) : Option String :=
if s.all token ∧ ¬s.isEmpty then
if s.all tchar ∧ ¬s.isEmpty then
some s
else if s.all quotedStringChar then
some (.append
@@ -101,7 +101,7 @@ def unquoteHttpString? (s : String) : Option String :=
| .done _ | .invalid => .invalid) .start with
| .done result => some result
| _ => none
else if s.all Char.token then
else if s.all Char.tchar then
some s
else
none
@@ -112,6 +112,6 @@ 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.token
¬s.isEmpty ∧ s.all Char.tchar
end Std.Http.Internal

46
tests/lean/run/async_http_encode.lean
View File

@@ -116,7 +116,7 @@ info: "999 Unknown"
#guard_msgs in
#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩)
/-! ## Request.Head encoding -/
/-! ## Request.line encoding -/
/--
info: ""
@@ -160,7 +160,7 @@ info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
headers := Headers.empty.insert! "content-type" "application/json"
} : Request.Head)
/-! ## Response.Head encoding -/
/-! ## Response.line encoding -/
/--
info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
@@ -222,61 +222,61 @@ info: "a\x0d\n0123456789\x0d\n"
info: "GET /index.html HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.get (.parse! "/index.html") |>.body ()).head
#eval encodeStr (Request.get (.parse! "/index.html") |>.body ()).line
/--
info: "POST /api/data HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.post (.parse! "/api/data") |>.body ()).head
#eval encodeStr (Request.post (.parse! "/api/data") |>.body ()).line
/--
info: "PUT /resource HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.put (.parse! "/resource") |>.body ()).head
#eval encodeStr (Request.put (.parse! "/resource") |>.body ()).line
/--
info: "DELETE /item HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.delete (.parse! "/item") |>.body ()).head
#eval encodeStr (Request.delete (.parse! "/item") |>.body ()).line
/--
info: "PATCH /update HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.patch (.parse! "/update") |>.body ()).head
#eval encodeStr (Request.patch (.parse! "/update") |>.body ()).line
/--
info: "HEAD /check HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.head' (.parse! "/check") |>.body ()).head
#eval encodeStr (Request.head (.parse! "/check") |>.body ()).line
/--
info: "OPTIONS * HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.options (.parse! "*") |>.body ()).head
#eval encodeStr (Request.options (.parse! "*") |>.body ()).line
/--
info: "CONNECT proxy:8080 HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.connect (.parse! "proxy:8080") |>.body ()).head
#eval encodeStr (Request.connect (.parse! "proxy:8080") |>.body ()).line
/--
info: "TRACE /debug HTTP/1.1\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.trace (.parse! "/debug") |>.body ()).head
#eval encodeStr (Request.trace (.parse! "/debug") |>.body ()).line
/--
info: "POST /v2 HTTP/2.0\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.new |>.method .post |>.uri (.parse! "/v2") |>.version .v20 |>.body ()).head
#eval encodeStr (Request.new |>.method .post |>.uri (.parse! "/v2") |>.version .v20 |>.body ()).line
/-! ## Response builder -/
@@ -284,67 +284,67 @@ info: "POST /v2 HTTP/2.0\x0d\n\x0d\n"
info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.ok |>.body ()).head
#eval encodeStr (Response.ok |>.body ()).line
/--
info: "HTTP/1.1 404 Not Found\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.notFound |>.body ()).head
#eval encodeStr (Response.notFound |>.body ()).line
/--
info: "HTTP/1.1 500 Internal Server Error\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.internalServerError |>.body ()).head
#eval encodeStr (Response.internalServerError |>.body ()).line
/--
info: "HTTP/1.1 400 Bad Request\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.badRequest |>.body ()).head
#eval encodeStr (Response.badRequest |>.body ()).line
/--
info: "HTTP/1.1 201 Created\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.created |>.body ()).head
#eval encodeStr (Response.created |>.body ()).line
/--
info: "HTTP/1.1 202 Accepted\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.accepted |>.body ()).head
#eval encodeStr (Response.accepted |>.body ()).line
/--
info: "HTTP/1.1 401 Unauthorized\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.unauthorized |>.body ()).head
#eval encodeStr (Response.unauthorized |>.body ()).line
/--
info: "HTTP/1.1 403 Forbidden\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.forbidden |>.body ()).head
#eval encodeStr (Response.forbidden |>.body ()).line
/--
info: "HTTP/1.1 409 Conflict\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.conflict |>.body ()).head
#eval encodeStr (Response.conflict |>.body ()).line
/--
info: "HTTP/1.1 503 Service Unavailable\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.serviceUnavailable |>.body ()).head
#eval encodeStr (Response.serviceUnavailable |>.body ()).line
/--
info: "HTTP/1.1 418 I'm a teapot\x0d\n\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Response.withStatus .imATeapot |>.body ()).head
#eval encodeStr (Response.withStatus .imATeapot |>.body ()).line
/-! ## Edge cases: Status encoding -/