fix: size

src/Std/Internal/Http/Data/Headers/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Internal.Http.Data.Headers.Name
 public import Std.Internal.Http.Data.Headers.Value
+public import Std.Internal.Parsec.Basic
 
 public section
 
@@ -31,12 +32,12 @@ Typeclass for typed HTTP headers that can be parsed from and serialized to heade
 class Header (α : Type) where
 
   /--
-  Parse a header value into the typed representation.
+  Parses a header value into the typed representation.
   -/
   parse : Header.Value → Option α
 
   /--
-  Serialize the typed representation back to a name-value pair.
+  Serializes the typed representation back to a name-value pair.
   -/
   serialize : α → Header.Name × Header.Value
 
@@ -47,8 +48,13 @@ instance [h : Header α] : Encode .v11 α where
 
 namespace Header
 
-private def parseTokenList (v : Value) : Array String :=
-  v.value.split (· == ',') |>.toArray.map (·.trimAscii.toString.toLower)
+private def parseTokenList (v : Value) : Option (Array String) := do
+  let rawParts := v.value.split (· == ',')
+  let parts := rawParts.map (·.trimAscii)
+
+  guard (parts.all (¬·.isEmpty))
+
+  return parts.toArray.map (fun s => s.toString.toLower)
 
 /--
 The `Content-Length` header, representing the size of the message body in bytes.
@@ -124,7 +130,7 @@ structure TransferEncoding where
   /--
   Proof that the transfer codings satisfy the chunked placement rules.
   -/
-  valid : TransferEncoding.Validate codings = true
+  isValid : TransferEncoding.Validate codings = true
 
 deriving Repr
 
@@ -139,8 +145,8 @@ def isChunked (te : TransferEncoding) : Bool :=
 /--
 Parses a comma-separated list of transfer codings from a header value, validating chunked placement.
 -/
-def parse (v : Value) : Option TransferEncoding :=
-  let codings := parseTokenList v
+def parse (v : Value) : Option TransferEncoding := do
+  let codings ← parseTokenList v
   if h : TransferEncoding.Validate codings then
     some ⟨codings, h⟩
   else
@@ -192,8 +198,8 @@ def shouldClose (connection : Connection) : Bool :=
 /--
 Parses a `Connection` header value into normalized tokens.
 -/
-def parse (v : Value) : Option Connection :=
-  let tokens := parseTokenList v
+def parse (v : Value) : Option Connection := do
+  let tokens ← parseTokenList v
   if h : tokens.all isToken = true then
     some ⟨tokens, h⟩
   else

src/Std/Internal/Http/Internal/LowerCase.lean

@@ -63,4 +63,6 @@ theorem isLowerCase_toLower {s : String} : IsLowerCase s.toLower := by
 theorem isLowerCase_empty : IsLowerCase "" := by
   simp [IsLowerCase, String.toLower]
 
-end Std.Http.Internal.IsLowerCase
+end IsLowerCase
+
+end Std.Http.Internal

src/Std/Internal/Http/Internal/MultiMap.lean

@@ -27,9 +27,7 @@ open Std Internal
 set_option linter.all true
 
 /--
-A structure for managing key-value pairs where each key can have multiple values.
-Invariant: each key must have at least one value, and all indices stored in `index`
-are valid positions into `entries`.
+A structure for managing ordered key-value pairs where each key can have multiple values.
 -/
 structure MultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
 
@@ -195,7 +193,8 @@ If the key is absent, returns the map unchanged.
 -/
 @[inline]
 def update [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) (f : β → β) : MultiMap α β :=
-  if key ∉ map then map
+  if key ∉ map then
+    map
   else
     map.entries.foldl (fun acc (k, v) => acc.insert k (if k == key then f v else v)) empty
 
@@ -233,18 +232,18 @@ def erase [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) :
     |>.foldl (fun acc (k, v) => acc.insert k v) empty
 
 /--
-Gets the number of keys in the map.
+Gets the number of entries in the map.
 -/
 @[inline]
 def size (map : MultiMap α β) : Nat :=
-  map.indexes.size
+  map.entries.size
 
 /--
 Checks if the map is empty.
 -/
 @[inline]
 def isEmpty (map : MultiMap α β) : Bool :=
-  map.indexes.isEmpty
+  map.entries.isEmpty
 
 /--
 Converts the multimap to an array of key-value pairs (flattened).