Merge branch 'master' into mvcgen-invariant-attr

src/Lean/CoreM.lean

@@ -431,6 +431,10 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
 
+/--
+Run a `CoreM` monad in IO.
+Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.getNumHeartbeats`.
+-/
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => throw <| IO.userError (← msg.toString)
@@ -440,7 +444,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
--- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 

src/Lean/Data/Name.lean

@@ -205,7 +205,7 @@ def anyS (n : Name) (f : String → Bool) : Bool :=
 /-- Return true if the name is in a namespace associated to metaprogramming. -/
 def isMetaprogramming (n : Name) : Bool :=
   let components := n.components
-  components.head? == some `Lean || (components.any fun n => n == `Tactic || n == `Linter)
+  components.head?.any (· == `Lean) || (components.any (· matches `Tactic | `Linter | `Simproc | `Meta))
 
 end Name
 end Lean

src/Lean/Elab/BuiltinDo/Let.lean

@@ -145,13 +145,13 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
       | _, _ => pure xType?
     elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x <| dec.continueWithUnit)
       (kind := dec.kind)
-  | `(doPatDecl| _%$pattern ← $rhs) =>
+  | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x none rhs dec.continueWithUnit (kind := dec.kind)
-  | `(doPatDecl| $pattern:term ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
+  | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
     let rest? := rest?.join
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x none rhs do
+    elabDoIdDecl x patType? rhs do
       match letOrReassign, otherwise? with
       | .let mutTk?, some otherwise =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec

src/Lean/Elab/Do/InferControlInfo.lean

@@ -184,7 +184,7 @@ partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDe
   | `(doIdDecl| $x:ident $[: $_]? ← $rhs) =>
     let reassigns := if reassignment then #[x] else #[]
     ofLetOrReassign reassigns rhs none none
-  | `(doPatDecl| $pattern ← $rhs $[| $otherwise? $[$body??]?]?) =>
+  | `(doPatDecl| $pattern $[: $_]? ← $rhs $[| $otherwise? $[$body??]?]?) =>
     let reassigns ← if reassignment then getPatternVarsEx pattern else pure #[]
     ofLetOrReassign reassigns rhs otherwise? body??.join
   | _ => throwError "Not a let or reassignment declaration: {toString decl}"

src/Lean/Elab/Do/Legacy.lean

@@ -722,7 +722,7 @@ def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
 def getDoIdDeclVar (doIdDecl : Syntax) : Var :=
   doIdDecl[0]
 
--- termParser >> leftArrow >> termParser >> optional (" | " >> termParser)
+-- termParser >> optType >> leftArrow >> termParser >> optional (" | " >> termParser)
 def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := doPatDecl[0]
   getPatternVarsEx pattern
@@ -1420,7 +1420,7 @@ mutual
      where
      ```
      def doIdDecl   := leading_parser ident >> optType >> leftArrow >> doElemParser
-     def doPatDecl  := leading_parser termParser >> leftArrow >> doElemParser >> optional ((" | " >> doSeq) >> optional doSeq)
+     def doPatDecl  := leading_parser termParser >> optType >> leftArrow >> doElemParser >> optional ((" | " >> doSeq) >> optional doSeq)
      ```
   -/
   partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
@@ -1440,13 +1440,21 @@ mutual
         | kRef::_  => concat c kRef y k
     else if decl.getKind == ``Parser.Term.doPatDecl then
       let pattern := decl[0]
-      let doElem  := decl[2]
-      let optElse := decl[3]
+      let optType := decl[1]
+      let doElem  := decl[3]
+      let optElse := decl[4]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ← if isMutableLet doLetArrow then
-          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+        let auxDo ← if optType.isNone then
+          if isMutableLet doLetArrow then
+            `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+          else
+            `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow $pattern:term := __discr)
         else
-          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow $pattern:term := __discr)
+          let ty := optType[0][1]
+          if isMutableLet doLetArrow then
+            `(do let%$doLetArrow __discr : $ty ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+          else
+            `(do let%$doLetArrow __discr : $ty ← $doElem; let%$doLetArrow $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         let elseSeq := optElse[1]
@@ -1457,7 +1465,11 @@ mutual
         else
           pure (getDoSeqElems contSeq).toArray
         let contSeq := mkDoSeq contSeq
-        let auxDo ← `(do let%$doLetArrow __discr ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        let auxDo ← if optType.isNone then
+          `(do let%$doLetArrow __discr ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        else
+          let ty := optType[0][1]
+          `(do let%$doLetArrow __discr : $ty ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
     else
       throwError "unexpected kind of `do` declaration"
@@ -1492,10 +1504,15 @@ mutual
       doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
     else if decl.getKind == ``Parser.Term.doPatDecl then
       let pattern := decl[0]
-      let doElem  := decl[2]
-      let optElse := decl[3]
+      let optType := decl[1]
+      let doElem  := decl[3]
+      let optElse := decl[4]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ← `(do let __discr ← $doElem; $pattern:term := __discr)
+        let auxDo ← if optType.isNone then
+          `(do let __discr ← $doElem; $pattern:term := __discr)
+        else
+          let ty := optType[0][1]
+          `(do let __discr : $ty ← $doElem; $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         throwError "reassignment with `|` (i.e., \"else clause\") is not currently supported"

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Core.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Init.Sym.Lemmas
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+
+namespace Lean.Meta.Sym.Simp
+
+/-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
+if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
+builtin_cbv_simproc ↓ simpOr (@Or _ _) := fun e => do
+  let_expr Or a b := e | return .rfl
+  match (← simp a) with
+  | .rfl _ =>
+    if (← isTrueExpr a) then
+      return .step (← getTrueExpr) (mkApp (mkConst ``true_or) b) (done := true)
+    else if (← isFalseExpr a) then
+      return .step b (mkApp (mkConst ``false_or) b)
+    else
+      return .rfl
+  | .step a' ha _ =>
+    if (← isTrueExpr a') then
+      return .step (← getTrueExpr) (mkApp (e.replaceFn ``Sym.or_eq_true_left) ha) (done := true)
+    else if (← isFalseExpr a') then
+      return .step b (mkApp (e.replaceFn ``Sym.or_eq_right) ha)
+    else
+      return .rfl
+
+/-- Short-circuit evaluation of `And`. Simplifies only the left argument;
+if it reduces to `False`, returns `False` immediately without evaluating the right side. -/
+builtin_cbv_simproc ↓ simpAnd (@And _ _) := fun e => do
+  let_expr And a b := e | return .rfl
+  match (← simp a) with
+  | .rfl _ =>
+    if (← isFalseExpr a) then
+      return .step (← getFalseExpr) (mkApp (mkConst ``false_and) b) (done := true)
+    else if (← isTrueExpr a) then
+      return .step b (mkApp (mkConst ``true_and) b)
+    else
+      return .rfl
+  | .step a' ha _ =>
+    if (← isFalseExpr a') then
+      return .step (← getFalseExpr) (mkApp (e.replaceFn ``Sym.and_eq_false_left) ha) (done := true)
+    else if (← isTrueExpr a') then
+      return .step b (mkApp (e.replaceFn ``Sym.and_eq_left) ha)
+    else
+      return .rfl
+
+end Lean.Meta.Sym.Simp

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -21,6 +21,8 @@ import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.Opaque
 import Lean.Meta.Tactic.Cbv.CbvEvalExt
 import Lean.Compiler.NoncomputableAttr
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
 
 /-!
 # Control Flow Handling for Cbv
@@ -81,7 +83,7 @@ def simpAndMatchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback
 
 /-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
-public def simpIteCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 5) fun e => do
@@ -149,7 +151,7 @@ def simpAndMatchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback
 
 /-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
-public def simpDIteCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDIteCbv (@dite _ _ _ _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 5) fun e => do
@@ -187,46 +189,6 @@ public def simpDIteCbv : Simproc := fun e => do
             let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
             return .step e' h' (done := true)
 
-/-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
-if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
-public def simpOr : Simproc := fun e => do
-  let_expr Or a b := e | return .rfl
-  match (← simp a) with
-  | .rfl _ =>
-    if (← isTrueExpr a) then
-      return .step (← getTrueExpr) (mkApp (mkConst ``true_or) b) (done := true)
-    else if (← isFalseExpr a) then
-      return .step b (mkApp (mkConst ``false_or) b)
-    else
-      return .rfl
-  | .step a' ha _ =>
-    if (← isTrueExpr a') then
-      return .step (← getTrueExpr) (mkApp (e.replaceFn ``Sym.or_eq_true_left) ha) (done := true)
-    else if (← isFalseExpr a') then
-      return .step b (mkApp (e.replaceFn ``Sym.or_eq_right) ha)
-    else
-      return .rfl
-
-/-- Short-circuit evaluation of `And`. Simplifies only the left argument;
-if it reduces to `False`, returns `False` immediately without evaluating the right side. -/
-public def simpAnd : Simproc := fun e => do
-  let_expr And a b := e | return .rfl
-  match (← simp a) with
-  | .rfl _ =>
-    if (← isFalseExpr a) then
-      return .step (← getFalseExpr) (mkApp (mkConst ``false_and) b) (done := true)
-    else if (← isTrueExpr a) then
-      return .step b (mkApp (mkConst ``true_and) b)
-    else
-      return .rfl
-  | .step a' ha _ =>
-    if (← isFalseExpr a') then
-      return .step (← getFalseExpr) (mkApp (e.replaceFn ``Sym.and_eq_false_left) ha) (done := true)
-    else if (← isTrueExpr a') then
-      return .step b (mkApp (e.replaceFn ``Sym.and_eq_left) ha)
-    else
-      return .rfl
-
 /-- Reduce `decide` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
 def matchDecideDecidable (p inst instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
   match_expr instToMatch with
@@ -264,7 +226,7 @@ corresponding boolean directly. Otherwise, simplifies the `Decidable` instance a
 on `isTrue`/`isFalse` to determine the boolean value. When `p` simplified to a new `p'`
 but the instance doesn't reduce to `isTrue`/`isFalse`, falls back to rebuilding
 `decide p'` with a congruence proof. -/
-public def simpDecideCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDecideCbv (@Decidable.decide _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 2 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 2) fun e => do
@@ -320,9 +282,7 @@ public def withCbvOpaqueGuard (x : MetaM α) : MetaM α := do
         else return false
   ) x
 
-def tryMatchEquations (appFn : Name) : Simproc := fun e => do
-  let thms ← getMatchTheorems appFn
-  thms.rewrite (d := dischargeNone) e
+builtin_cbv_simproc ↓ simpCbvCond (@cond _ _ _) := simpCond
 
 public def reduceRecMatcher : Simproc := fun e => do
   if let some e' ← withCbvOpaqueGuard <| reduceRecMatcher? e then
@@ -330,7 +290,16 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-def tryMatcher : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
+  (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
+
+def tryMatchEquations (appFn : Name) : Simproc := fun e => do
+  let thms ← getMatchTheorems appFn
+  thms.rewrite (d := dischargeNone) e
+
+/-- Dispatch control flow constructs to their specialized simprocs.
+Precondition: `e` is an application. -/
+public def tryMatcher : Simproc := fun e => do
   unless e.isApp do
     return .rfl
   let some appFn := e.getAppFn.constName? | return .rfl
@@ -342,26 +311,4 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
-/-- Dispatch control flow constructs to their specialized simprocs.
-Precondition: `e` is an application. -/
-public def simpControlCbv : Simproc := fun e => do
-  let .const declName _ := e.getAppFn | return .rfl
-  if declName == ``ite then
-    simpIteCbv e
-  else if declName == ``cond then
-    simpCond e
-  else if declName == ``dite then
-    simpDIteCbv e
-  else if declName == ``Decidable.rec then
-    -- We force the rewrite in the last argument, so that we can unfold the `Decidable` instance.
-    (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher <| e
-  else if declName == ``Or then
-    simpOr e
-  else if declName == ``And then
-    simpAnd e
-  else if declName == ``Decidable.decide then
-    simpDecideCbv e
-  else
-    tryMatcher e
-
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -10,6 +10,7 @@ prelude
 public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Tactic.Cbv.Opaque
 public import Lean.Meta.Tactic.Cbv.ControlFlow
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Core
 import Lean.Meta.Tactic.Cbv.Util
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.CbvEvalExt
@@ -263,7 +264,7 @@ def cbvPreStep : Simproc := fun e => do
   | .lit .. => foldLit e
   | .proj .. => handleProj e
   | .const .. => isOpaqueConst >> handleConst <| e
-  | .app .. => simpControlCbv <|> simplifyAppFn <| e
+  | .app .. => tryMatcher <|> simplifyAppFn <| e
   | .letE .. =>
     if e.letNondep! then
       let betaAppResult ← toBetaApp e

src/Lean/Parser/Do.lean

@@ -86,7 +86,7 @@ def doIdDecl   := leading_parser
   atomic (ident >> optType >> ppSpace >> leftArrow) >>
   doElemParser
 def doPatDecl  := leading_parser
-  atomic (termParser >> ppSpace >> leftArrow) >>
+  atomic (termParser >> optType >> ppSpace >> leftArrow) >>
   doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent))
 @[builtin_doElem_parser] def doLetArrow      := leading_parser withPosition <|
   "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)

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