fix: remove use of native_decide in the HTTP library (#12857)

This PR removes the use of `native_decide` in the HTTP library and adds
proofs to remove the `panic!`.

src/Std/Internal/Http/Data/Chunk.lean

@@ -87,13 +87,13 @@ def ofString! (s : String) : ExtensionName :=
 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.
+A proposition asserting that `s` is a valid extension value, meaning every character passes
+`Char.quotedStringChar` (i.e. is `qdtext` or a valid `quoted-pair` payload).
 
 Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
 -/
 abbrev IsValidExtensionValue (s : String) : Prop :=
-  (quoteHttpString? s).isSome
+  s.toList.all Char.quotedStringChar
 
 /--
 A validated chunk extension value that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1.
@@ -115,30 +115,29 @@ structure ExtensionValue where
   /--
   The proof that it's a valid extension value.
   -/
-  validExtensionValue : IsValidExtensionValue value := by decide
+  isValidExtensionValue : IsValidExtensionValue value := by decide
 deriving Repr, DecidableEq, BEq
 
 namespace ExtensionValue
 
 instance : Inhabited ExtensionValue where
-  default := ⟨"", by native_decide⟩
+  default := ⟨"", by 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
+  quoteHttpString s.value s.isValidExtensionValue
 
 /--
 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
+  if h : IsValidExtensionValue s then
     some ⟨s, h⟩
   else
     none

src/Std/Internal/Http/Internal/Char.lean

@@ -6,7 +6,10 @@ Authors: Sofia Rodrigues
 module
 
 prelude
+public import Init.Data.Char
 public import Init.Data.String
+public import Init.Data.Int
+public import Init.Grind
 
 @[expose]
 public section
@@ -97,6 +100,24 @@ quoted-string body character class:
 def quotedStringChar (c : Char) : Bool :=
   qdtext c || quotedPairChar c
 
+theorem quotedStringChar_lt_0x80 : quotedStringChar c → c < '\x80' := by
+  simp [quotedStringChar, qdtext, quotedPairChar]
+  split <;> simp only [true_or, Char.reduceLT, imp_self]
+  grind [→ Char.le_def.mp, Char.lt_def.mpr, vchar]
+
+private theorem not_quotedStringChar_ofNat_aux :
+    ∀ c : Nat, c < 128 → ¬(qdtext (Char.ofNat c)) ∧ ¬((Char.ofNat c = '\"') ∨ (Char.ofNat c = '\\')) →
+    ¬(quotedStringChar (Char.ofNat c)) := by
+  decide
+
+theorem not_quotedStringChar_of_not_qdtext_not_dquote_backslash :
+    ∀ c : Char, c < '\x80' → ¬(qdtext (c)) ∧ ¬((c = '\"') || (c = '\\')) →
+    ¬(quotedStringChar c) := by
+  intro c hlt hq
+  simpa [Char.ofNat_toNat] using
+    (not_quotedStringChar_ofNat_aux
+      c.toNat hlt (by simpa [Char.ofNat_toNat] using hq))
+
 /--
 field-vchar = VCHAR
 ; ASCII-only variant (no obs-text).

src/Std/Internal/Http/Internal/String.lean

@@ -27,42 +27,49 @@ open Char
 set_option linter.all true
 
 /--
-Core character quoting used by `String.quote`.
+Core character quoting used by `quoteHttpString`.
 
-In string context (`inString := true`), this emits:
-- `qdtext` characters directly
-- `"` and `\\` as `quoted-pair`
-and panics for characters outside the grammar.
+Emits `qdtext` characters directly and `"` / `\\` as `quoted-pair`.
+The proof `h₀ : quotedStringChar c` guarantees the impossible branch is unreachable.
 -/
-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"
+def quoteCore (c : Char) (h₀ : quotedStringChar c) : String :=
+  if h : qdtext c then
+    .singleton c
+  else if h₁ : c = '\"' || c = '\\' then
+    .append "\\" (.singleton c)
   else
-    if quotedPairChar c then
-      .singleton c
-    else
-      panic! "invalid HTTP quoted-pair content"
+    absurd h₀ (not_quotedStringChar_of_not_qdtext_not_dquote_backslash _ (quotedStringChar_lt_0x80 h₀) ⟨h, h₁⟩)
 
 /--
-Attempts to quote `s` as an HTTP `quoted-string`:
-`DQUOTE *( qdtext / quoted-pair ) DQUOTE`.
+Quotes `s` as an HTTP `quoted-string`: `DQUOTE *( qdtext / quoted-pair ) DQUOTE`.
 
-Returns `none` when any character in `s` cannot be represented by the grammar.
+If every character is a `tchar` and the string is non-empty, the string is returned as-is (it is
+already a valid token). Otherwise the string is wrapped in double quotes, escaping `"` and `\`
+as `quoted-pair`.
+
+Requires a proof that every character passes `quotedStringChar`.
 -/
 @[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)
+def quoteHttpString (s : String) (h : s.toList.all quotedStringChar) : String :=
+  let sl := s.toList.attach
+
+  if sl.all (tchar ·.val) ∧ ¬sl.isEmpty then
+    s
+  else
+    (.append
+      (sl.foldl (fun acc x =>
+        .append acc (quoteCore x.val (List.all_eq_true.mp h x.val x.2))) "\"")
       "\"")
+
+/--
+Attempts to quote `s` as an HTTP `quoted-string`.
+
+Returns `some` with the quoted result when every character passes `quotedStringChar`, or `none`
+when any character cannot be represented by the grammar.
+-/
+def quoteHttpString? (s : String) : Option String :=
+  if h : s.toList.all quotedStringChar then
+    some <| quoteHttpString s h
   else
     none