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

fix: suggestions

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 10:11:25 -03:00
parent a086a817e0
commit d41753a5f9
7 changed files with 114 additions and 376 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

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

@@ -59,7 +59,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.
@@ -79,7 +79,7 @@ structure Request.Builder where
/--
The head of the request.
-/
head : Head := { method := .get, version := .v11, uri := "*" }
line : Head := { method := .get, version := .v11, uri := "*" }
/--
Optional dynamic metadata attached to the request.
@@ -123,19 +123,19 @@ 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 : String) : Builder :=
{ builder with head := { builder.head with uri := uri } }
{ builder with line := { builder.line with uri := uri } }
/--
Inserts a typed extension value into the request being built.
@@ -147,7 +147,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
@@ -193,9 +193,8 @@ def patch (uri : String) : 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 : String) : Builder :=
def head (uri : String) : Builder :=
new
|>.method .head
|>.uri uri

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

@@ -45,7 +45,7 @@ structure Response (t : Type) where
/--
The response status-line information.
-/
head : Response.Head := {}
line : Response.Head := {}
/--
The content of the response.
@@ -118,14 +118,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.head, 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.head, 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

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

@@ -27,49 +27,15 @@ set_option linter.all true
Checks if a character is ASCII (Unicode code point < 128).
-/
@[expose]
def isAscii (c : Char) : Bool :=
c.toNat < 128
/--
Checks if a character is a decimal digit (0-9).
-/
@[inline, expose]
def isDigitChar (c : Char) : Bool :=
c ≥ '0' ∧ c ≤ '9'
/--
Checks if a character is an alphabetic character (a-z or A-Z).
-/
@[inline, expose]
def isAlphaChar (c : Char) : Bool :=
(c ≥ 'A' ∧ c ≤ 'Z') ∨ (c ≥ 'a' ∧ c ≤ 'z')
def isAscii (ch : Char) : Bool :=
ch.toNat < 128
/--
Checks if a byte represents an ASCII character (value < 128).
-/
@[expose]
def isAsciiByte (c : UInt8) : Bool :=
c < 128
/--
Checks if a byte is a decimal digit (0-9).
-/
@[inline, expose]
def isDigit (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 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)
def isAsciiByte (ch : Char) : Bool :=
isAscii ch
/--
tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
@@ -77,185 +43,106 @@ tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
/ DIGIT / ALPHA
; Visible token characters used to build `token`.
-/
def tchar (c : Char) : Bool :=
"!#$%&'*+-.^_`|~".toList.contains c
∨ isDigitChar c
∨ isAlphaChar c
def tchar (ch : Char) : Bool :=
ch matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' |
'+' | '-' | '.' | '^' | '_' | '`' | '|' | '~' ||
Char.isDigit ch || Char.isAlpha ch
/--
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
def token (ch : Char) : Bool :=
ch matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' |
'+' | '-' | '.' | '^' | '_' | '`' | '|' | '~' ||
Char.isDigit ch || Char.isAlpha ch
/--
vchar = %x21-7E
; Visible (printing) ASCII characters.
-/
def vcharSpec (c : Char) : Bool :=
c ≥ '!' ∧ c ≤ '~'
/--
Checks if `c` is a visible (printing) ASCII character.
-/
def vchar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
theorem vchar_eq_vcharSpec_on_ascii : EqOnAscii vchar vcharSpec := by
decide
def vchar (ch : Char) : Bool :=
ch ≥ '!' && ch ≤ '~'
/--
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 ≤ '[') ∨
(']' ≤ 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
def qdtext (ch : Char) : Bool :=
ch matches '\t' | ' ' | '!' ||
('#' ≤ ch && ch ≤ '[') ||
(']' ≤ ch && ch ≤ '~')
/--
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).
-/
def quotedPairChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem quotedPairChar_eq_quotedPairCharSpec_on_ascii :
EqOnAscii quotedPairChar quotedPairCharSpec := by
decide
def quotedPairChar (ch : Char) : Bool :=
ch matches '\t' | ' ' || vchar ch
/--
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`.
-/
def quotedStringChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem quotedStringChar_eq_quotedStringCharSpec_on_ascii :
EqOnAscii quotedStringChar quotedStringCharSpec := by
decide
def quotedStringChar (ch : Char) : Bool :=
qdtext ch || quotedPairChar ch
/--
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.
-/
def fieldVchar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
theorem fieldVchar_eq_fieldVcharSpec_on_ascii : EqOnAscii fieldVchar fieldVcharSpec := by
decide
def fieldVchar (ch : Char) : Bool :=
vchar ch
/--
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).
-/
def fieldContent (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem fieldContent_eq_fieldContentSpec_on_ascii : EqOnAscii fieldContent fieldContentSpec := by
decide
def fieldContent (ch : Char) : Bool :=
fieldVchar ch || ch 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).
-/
def ctext (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffeffffffffffffcff00000200 c.toNat
theorem ctext_eq_ctextSpec_on_ascii : EqOnAscii ctext ctextSpec := by
decide
def ctext (ch : Char) : Bool :=
ch matches '\t' | ' ' ||
('!' ≤ ch && ch ≤ '\'') ||
('*' ≤ ch && ch ≤ '[') ||
(']' ≤ ch && ch ≤ '~')
/--
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).
-/
def etagc (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffa00000000 c.toNat
theorem etagc_eq_etagcSpec_on_ascii : EqOnAscii etagc etagcSpec := by
decide
def etagc (ch : Char) : Bool :=
ch matches '!' || ('#' ≤ ch && ch ≤ '~')
/--
OWS = *( SP / HTAB ) (character class only)
-/
def ows (c : Char) : Bool :=
c = ' ' ∨ c = '\t'
def ows (ch : Char) : Bool :=
ch matches ' ' | '\t'
/--
BWS = OWS (character class alias)
-/
def bws (c : Char) : Bool :=
ows c
def bws (ch : Char) : Bool :=
ows ch
/--
RWS = 1*( SP / HTAB ) (character class is identical to `ows`)
-/
def rws (c : Char) : Bool :=
ows c
def rws (ch : Char) : Bool :=
ows ch
/--
obs-text = %x80-FF (and higher Unicode scalar values in this library's `Char` model).
-/
def obsText (c : Char) : Bool :=
0x80 ≤ c.toNat
def obsText (ch : Char) : Bool :=
0x80 ≤ ch.toNat
/--
reason-phrase character class:
@@ -264,239 +151,103 @@ 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.
-/
def reasonPhraseChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
theorem reasonPhraseChar_eq_reasonPhraseCharSpec : EqOnAscii reasonPhraseChar reasonPhraseCharSpec := by
decide
/--
Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F) using a precomputed bitmask.
-/
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]
def isHexDigit (c : Char) : Bool :=
Nat.testBit 0x0000007e0000007e03ff000000000000 c.toNat
theorem isHexDigit_eq_isHexDigitSpec_on_ascii : EqOnAscii isHexDigit isHexDigitSpec := by
decide
def reasonPhraseChar (ch : Char) : Bool :=
ch matches '\t' | ' ' || vchar ch
/--
Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
-/
@[expose]
def isHexDigitByte (c : UInt8) : Bool :=
(c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
(c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) ||
(c ≥ 'A'.toUInt8 && c ≤ 'F'.toUInt8)
def isHexDigit (ch : Char) : Bool :=
(ch ≥ '0' && ch ≤ '9') ||
(ch ≥ 'a' && ch ≤ 'f') ||
(ch ≥ 'A' && ch ≤ 'F')
/--
Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
-/
def isAlphaNumSpec (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.
Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
-/
@[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
def isHexDigitByte (ch : Char) : Bool :=
isHexDigit ch
/--
Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
Checks if `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
def isAsciiAlphaNumChar (ch : Char) : Bool :=
isAscii ch && Char.isAlphanum ch
/--
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 == '.'
/--
Checks if a character is valid after the first character of a URI scheme.
Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
-/
def isValidSchemeChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff680000000000 c.toNat
theorem isValidSchemeCharChar_eq_isValidSchemeCharCharSpec_on_ascii :
EqOnAscii isValidSchemeChar isValidSchemeCharSpec := by
decide
def isValidSchemeChar (ch : Char) : Bool :=
isAsciiAlphaNumChar ch || ch 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 == '.'
def isValidDomainNameChar (ch : Char) : Bool :=
isAsciiAlphaNumChar ch || ch matches '-' | '.'
/--
Checks if a character is valid for use in a domain name.
-/
def isValidDomainNameChar (c : Char) : Bool :=
isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff600000000000 c.toNat
theorem isValidDomainNameChar_eq_isValidDomainNameCharSpec_on_ascii :
EqOnAscii isValidDomainNameChar isValidDomainNameCharSpec := by
decide
/--
Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are:
Checks if a character 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]
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
def isUnreserved (ch : Char) : Bool :=
Char.isAlphanum ch || ch matches '-' | '.' | '_' | '~'
/--
Checks if a byte is a sub-delimiter character according to RFC 3986.
Checks if a character 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 ||
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
def isSubDelims (ch : Char) : Bool :=
ch matches '!' | '$' | '&' | '\'' | '(' | ')' | '*' | '+' | ',' | ';' | '='
/--
Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
Checks if a character 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.
-/
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]
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
def isPChar (ch : Char) : Bool :=
isUnreserved ch || isSubDelims ch || ch matches ':' | '@'
/--
Checks if a byte is a valid character in a URI query component according to RFC 3986.
Checks if a character 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]
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
def isQueryChar (ch : Char) : Bool :=
isPChar ch || ch matches '/' | '?'
/--
Checks if a byte is a valid character in a URI fragment component according to RFC 3986.
Checks if a character 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]
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
def isFragmentChar (ch : Char) : Bool :=
isPChar ch || ch matches '/' | '?'
/--
Checks if a byte is a valid character in a URI userinfo component according to RFC 3986.
Checks if a character 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.
-/
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]
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
def isUserInfoChar (ch : Char) : Bool :=
isUnreserved ch || isSubDelims ch || ch matches ':'
end Std.Http.Internal.Char

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

@@ -40,7 +40,7 @@ info: "GET"
info: "HEAD"
-/
#guard_msgs in
#eval encodeStr Method.head
#eval encodeStr Method.line
/--
info: "POST"
@@ -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: "GET /path HTTP/1.1\x0d\n"
@@ -140,7 +140,7 @@ info: "PUT /resource HTTP/2.0\x0d\n"
uri := "/resource"
} : Request.Head)
/-! ## Response.Head encoding -/
/-! ## Response.line encoding -/
/--
info: "HTTP/1.1 200 OK\x0d\n"
@@ -201,61 +201,61 @@ info: "a\x0d\n0123456789\x0d\n"
info: "GET /index.html HTTP/1.1\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.get "/index.html" |>.body ()).head
#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 ()).head
#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 ()).head
#eval encodeStr (Request.put "/resource" |>.body ()).line
/--
info: "DELETE /item HTTP/1.1\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.delete "/item" |>.body ()).head
#eval encodeStr (Request.delete "/item" |>.body ()).line
/--
info: "PATCH /update HTTP/1.1\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.patch "/update" |>.body ()).head
#eval encodeStr (Request.patch "/update" |>.body ()).line
/--
info: "HEAD /check HTTP/1.1\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.head' "/check" |>.body ()).head
#eval encodeStr (Request.head "/check" |>.body ()).line
/--
info: "OPTIONS * HTTP/1.1\x0d\n"
-/
#guard_msgs in
#eval encodeStr (Request.options "*" |>.body ()).head
#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 ()).head
#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 ()).head
#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 ()).head
#eval encodeStr (Request.new |>.method .post |>.uri "/v2" |>.version .v20 |>.body ()).line
/-! ## Response builder -/
@@ -263,67 +263,67 @@ info: "POST /v2 HTTP/2.0\x0d\n"
info: "HTTP/1.1 200 OK\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"
-/
#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"
-/
#guard_msgs in
#eval encodeStr (Response.internalServerError |>.body ()).head
#eval encodeStr (Response.internalServerError |>.body ()).line
/--
info: "HTTP/1.1 400 Bad Request\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"
-/
#guard_msgs in
#eval encodeStr (Response.created |>.body ()).head
#eval encodeStr (Response.created |>.body ()).line
/--
info: "HTTP/1.1 202 Accepted\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"
-/
#guard_msgs in
#eval encodeStr (Response.unauthorized |>.body ()).head
#eval encodeStr (Response.unauthorized |>.body ()).line
/--
info: "HTTP/1.1 403 Forbidden\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"
-/
#guard_msgs in
#eval encodeStr (Response.conflict |>.body ()).head
#eval encodeStr (Response.conflict |>.body ()).line
/--
info: "HTTP/1.1 503 Service Unavailable\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"
-/
#guard_msgs in
#eval encodeStr (Response.withStatus .imATeapot |>.body ()).head
#eval encodeStr (Response.withStatus .imATeapot |>.body ()).line
/-! ## Edge cases: Status encoding -/