feat: ConnState proofs, Huffman O(1) trie, xDS JSON parser, streaming StreamCallContext (v1.5.0)

CHANGELOG.md

@@ -1,6 +1,44 @@
 # Changelog
 
-All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.3.0**). Git tags such as `v1.3.0` are created manually by maintainers when publishing.
+All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.5.0**). Git tags such as `v1.5.0` are created manually by maintainers when publishing.
+
+## [1.5.0] — 2026-08-12
+
+Three sequenced engineering tranches: ConnState proof foundations (v1.4.0), security hardening LGSEC-2026-23 + LGSEC-2026-32 (v1.4.1), and streaming `ServerCallContext` for mTLS IAM parity (v1.5.0).
+
+### Tranche 1 — `H2.ConnState` proof foundations (was v1.4.0)
+
+New `Proofs/ConnState.lean` — zero `sorry`, CI-gated:
+
+- **CONTINUATION sequencing:** `handleFrame` rejects any non-CONTINUATION frame while `expectContinuation` is set; CONTINUATION for the wrong stream id is also a connection error.
+- **Non-negative recv windows:** `recvConnWindow` and per-stream `recvWindow` remain ≥ 0 after DATA within budget; DATA exceeding window triggers FLOW_CONTROL GOAWAY.
+- **`ENHANCE_YOUR_CALM`:** server rejects a header block exceeding `SETTINGS_MAX_HEADER_LIST_SIZE` with GOAWAY error code 0xb.
+- **GOAWAY gate:** `handleFrame` rejects new streams (id > `lastPeerStreamId`) and re-seen idle streams once `wentAway = true`; receiving a GOAWAY frame sets `wentAway`.
+
+### Tranche 2 — Security hardening (was v1.4.1)
+
+**LGSEC-2026-23 — Huffman decode-trie rewrite (`Hpack/Huffman.lean`):**
+- Replaced `O(n)` linear scan of `fullTable` per accumulated prefix with a pre-built `TrieRow` array sorted by code-length, enabling O(257) = O(1) per-symbol decode bounded by the fixed table size.
+- Fixed bit-accumulator mask bug (stale high bits above bit 29 now cleared with `&&& 0x3fffffff` after each consume).
+- Added `Hpack.Huffman.Error` `BEq`/`DecidableEq` instances.
+- New lemmas in `Proofs/Hpack.lean`: EOS symbol rejection, zero-padding rejection, valid-padding acceptance, and encode→decode roundtrip for "application/grpc".
+
+**LGSEC-2026-32 — xDS bootstrap JSON state-machine (`Grpc/Xds.lean`):**
+- Replaced the hand-rolled string scraper (`parseServerUris`, `parseBootstrap`) with a proper recursive-descent JSON parser: `parseVal` / inline array+object parsing consuming `fuel : Nat` for structural recursion.
+- Handles arbitrary whitespace, field reordering, `\"` escapes, nested objects, and unterminated-value attacks (returns `none` safely).
+- `parseEndpointsJson` also updated to use the new parser.
+
+### Tranche 3 — Streaming `ServerCallContext` (IAM parity, v1.5.0)
+
+**API additions (all additive):**
+- `Grpc.StreamCallContext` — alias for `ServerCallContext`; available in all streaming handler types.
+- `Stream.ServerStreamHandlerWithContext`, `Stream.ClientStreamHandlerWithContext`, `Stream.BidiStreamHandlerWithContext` — handler types carrying `StreamCallContext`.
+- `MethodHandler.serverStreamCtx`, `.clientStreamCtx`, `.bidiCtx` — new dispatch variants.
+- `Server.registerServerStreamWithContext`, `registerClientStreamWithContext`, `registerBidiWithContext` — streaming registration with context.
+- `Server.registerServerStreamTypedWithContext`, `registerClientStreamTypedWithContext`, `registerBidiTypedWithContext` — typed+decoded variants.
+- **Codegen:** `protoc-gen-lean4-grpc` now emits `register{Svc}{Method}ServerStreamWithContext`, `…ClientStreamWithContext`, `…BidiWithContext` alongside existing body-only registrars.
+
+Migration: fully additive — bump pin to `v1.5.0`. All existing `register*` APIs and handler types are unchanged; the `WithContext` variants are opt-in.
 
 ## [1.3.0] — 2026-08-11
 

Grpc.lean

@@ -39,5 +39,5 @@ import Grpc.Grpclb
 import Grpc.Interceptor
 
 namespace Grpc
-def version : String := "1.3.0"
+def version : String := "1.5.0"
 end Grpc

Grpc/Codegen/Emit.lean

@@ -455,6 +455,30 @@ def emitServiceTyped (pkg : String) (svc : ServiceDescriptor) : Except String St
         out := out ++ s!"    (h : Grpc.ServerCallContext → {reqTy} → IO ({respTy} × Grpc.Status)) : Grpc.Server :=\n"
         out := out ++ s!"  Grpc.Server.registerTypedWithContext s \"{full}\" \"{m.name}\"\n"
         out := out ++ s!"    {reqTy}.decode {respTy}.encode h\n\n"
+      else if !m.clientStreaming && m.serverStreaming then
+        let reqTy := localMessageName m.inputType
+        let respTy := localMessageName m.outputType
+        out := out ++ s!"/-- Register a typed server-streaming handler with `StreamCallContext` for `{svc.name}/{m.name}`. -/\n"
+        out := out ++ s!"def register{svc.name}{m.name}ServerStreamWithContext (s : Grpc.Server)\n"
+        out := out ++ s!"    (h : Grpc.StreamCallContext → {reqTy} → IO (Array {respTy} × Grpc.Status)) : Grpc.Server :=\n"
+        out := out ++ s!"  Grpc.Server.registerServerStreamTypedWithContext s \"{full}\" \"{m.name}\"\n"
+        out := out ++ s!"    {reqTy}.decode {respTy}.encode h\n\n"
+      else if m.clientStreaming && !m.serverStreaming then
+        let reqTy := localMessageName m.inputType
+        let respTy := localMessageName m.outputType
+        out := out ++ s!"/-- Register a typed client-streaming handler with `StreamCallContext` for `{svc.name}/{m.name}`. -/\n"
+        out := out ++ s!"def register{svc.name}{m.name}ClientStreamWithContext (s : Grpc.Server)\n"
+        out := out ++ s!"    (h : Grpc.StreamCallContext → Array {reqTy} → IO ({respTy} × Grpc.Status)) : Grpc.Server :=\n"
+        out := out ++ s!"  Grpc.Server.registerClientStreamTypedWithContext s \"{full}\" \"{m.name}\"\n"
+        out := out ++ s!"    {reqTy}.decode {respTy}.encode h\n\n"
+      else if m.clientStreaming && m.serverStreaming then
+        let reqTy := localMessageName m.inputType
+        let respTy := localMessageName m.outputType
+        out := out ++ s!"/-- Register a typed bidi-streaming handler with `StreamCallContext` for `{svc.name}/{m.name}`. -/\n"
+        out := out ++ s!"def register{svc.name}{m.name}BidiWithContext (s : Grpc.Server)\n"
+        out := out ++ s!"    (h : Grpc.StreamCallContext → Array {reqTy} → IO (Array {respTy} × Grpc.Status)) : Grpc.Server :=\n"
+        out := out ++ s!"  Grpc.Server.registerBidiTypedWithContext s \"{full}\" \"{m.name}\"\n"
+        out := out ++ s!"    {reqTy}.decode {respTy}.encode h\n\n"
     return out
 
 /-- Emit one `.lean` file's worth of message structs + typed client/server code for a single

Grpc/Metadata.lean

@@ -159,7 +159,7 @@ def methodGet : Hpack.HeaderField := ⟨ascii ":method", ascii "GET"⟩
 def schemeHttp : Hpack.HeaderField := ⟨ascii ":scheme", ascii "http"⟩
 def schemeHttps : Hpack.HeaderField := ⟨ascii ":scheme", ascii "https"⟩
 def teTrailers : Hpack.HeaderField := ⟨ascii "te", ascii "trailers"⟩
-def userAgent (version : String := "1.3.0") : Hpack.HeaderField :=
+def userAgent (version : String := "1.5.0") : Hpack.HeaderField :=
   ⟨ascii "user-agent", ascii s!"grpc-lean/{version}"⟩
 
 def http415 : Array Hpack.HeaderField :=

Grpc/PeerIdentity.lean

@@ -34,4 +34,8 @@ structure ServerCallContext where
   mtlsRequired : Bool := false
   deriving Inhabited
 
+/-- `StreamCallContext` is the same as `ServerCallContext`, available in streaming handlers
+    for mTLS peer identity and inbound metadata (IAM parity with unary context). -/
+abbrev StreamCallContext := ServerCallContext
+
 end Grpc

Grpc/Server.lean

@@ -31,6 +31,10 @@ inductive MethodHandler where
   | serverStream (h : Stream.ServerStreamHandler)
   | clientStream (h : Stream.ClientStreamHandler)
   | bidi (h : Stream.BidiStreamHandler)
+  /-- Context-aware streaming variants (v1.5.0 — mTLS IAM parity). -/
+  | serverStreamCtx (h : Stream.ServerStreamHandlerWithContext)
+  | clientStreamCtx (h : Stream.ClientStreamHandlerWithContext)
+  | bidiCtx (h : Stream.BidiStreamHandlerWithContext)
 
 structure ServiceMethod where
   service : String
@@ -63,6 +67,21 @@ def registerClientStream (s : Server) (service method : String) (h : Stream.Clie
 def registerBidi (s : Server) (service method : String) (h : Stream.BidiStreamHandler) : Server :=
   { s with methods := s.methods.push ⟨service, method, .bidi h⟩ }
 
+/-- Register a server-streaming handler with `StreamCallContext` (mTLS IAM parity, v1.5.0). -/
+def registerServerStreamWithContext (s : Server) (service method : String)
+    (h : Stream.ServerStreamHandlerWithContext) : Server :=
+  { s with methods := s.methods.push ⟨service, method, .serverStreamCtx h⟩ }
+
+/-- Register a client-streaming handler with `StreamCallContext`. -/
+def registerClientStreamWithContext (s : Server) (service method : String)
+    (h : Stream.ClientStreamHandlerWithContext) : Server :=
+  { s with methods := s.methods.push ⟨service, method, .clientStreamCtx h⟩ }
+
+/-- Register a bidi-streaming handler with `StreamCallContext`. -/
+def registerBidiWithContext (s : Server) (service method : String)
+    (h : Stream.BidiStreamHandlerWithContext) : Server :=
+  { s with methods := s.methods.push ⟨service, method, .bidiCtx h⟩ }
+
 /-- Typed unary register: decode request, run handler, encode response. -/
 def registerTyped (s : Server) (service method : String)
     (decode : ByteArray → Except String α) (encode : β → ByteArray)
@@ -85,6 +104,43 @@ def registerTypedWithContext (s : Server) (service method : String)
       let (resp, st) ← h ctx req
       return (encode resp, st)
 
+/-- Typed server-streaming register with `StreamCallContext`. -/
+def registerServerStreamTypedWithContext (s : Server) (service method : String)
+    (decode : ByteArray → Except String α) (encode : β → ByteArray)
+    (h : StreamCallContext → α → IO (Array β × Status)) : Server :=
+  registerServerStreamWithContext s service method fun ctx reqBytes => do
+    match decode reqBytes with
+    | .error e => return (#[], Status.invalidArgument e)
+    | .ok req =>
+      let (resps, st) ← h ctx req
+      return (resps.map encode, st)
+
+/-- Typed client-streaming register with `StreamCallContext`. -/
+def registerClientStreamTypedWithContext (s : Server) (service method : String)
+    (decode : ByteArray → Except String α) (encode : β → ByteArray)
+    (h : StreamCallContext → Array α → IO (β × Status)) : Server :=
+  registerClientStreamWithContext s service method fun ctx reqBytes => do
+    let mut reqs : Array α := #[]
+    for b in reqBytes do
+      match decode b with
+      | .error e => return (ByteArray.empty, Status.invalidArgument e)
+      | .ok r => reqs := reqs.push r
+    let (resp, st) ← h ctx reqs
+    return (encode resp, st)
+
+/-- Typed bidi-streaming register with `StreamCallContext`. -/
+def registerBidiTypedWithContext (s : Server) (service method : String)
+    (decode : ByteArray → Except String α) (encode : β → ByteArray)
+    (h : StreamCallContext → Array α → IO (Array β × Status)) : Server :=
+  registerBidiWithContext s service method fun ctx reqBytes => do
+    let mut reqs : Array α := #[]
+    for b in reqBytes do
+      match decode b with
+      | .error e => return (#[], Status.invalidArgument e)
+      | .ok r => reqs := reqs.push r
+    let (resps, st) ← h ctx reqs
+    return (resps.map encode, st)
+
 /-- Typed server-streaming register (still batch: one request → array of responses). -/
 def registerServerStreamTyped (s : Server) (service method : String)
     (decode : ByteArray → Except String α) (encode : β → ByteArray)
@@ -304,6 +360,49 @@ def handlerFor (s : Server) (peerIdentity : Option PeerIdentity := none)
             body := ← encodeManyIO msgs respAlg
             finished := false
           }
+      | .serverStreamCtx h =>
+        let req := payloads.getD 0 ByteArray.empty
+        let (msgs, st) ← h ctx req
+        return {
+          headers := respHeaders
+          body := ← encodeManyIO msgs respAlg
+          trailers := Metadata.statusHeaders st
+          finished := true
+        }
+      | .clientStreamCtx h =>
+        let (resp, st) ← h ctx payloads
+        let body ←
+          if st.code != .ok && resp.isEmpty then pure ByteArray.empty
+          else Message.encodeIO resp respAlg
+        return {
+          headers := respHeaders
+          body
+          trailers := Metadata.statusHeaders st
+          finished := true
+        }
+      | .bidiCtx h =>
+        if payloads.isEmpty then
+          if !endStream then
+            return { finished := false }
+          return {
+            headers := if headersSent then #[] else respHeaders
+            trailers := Metadata.statusHeaders Status.ok
+            finished := true
+          }
+        let (msgs, st) ← h ctx payloads
+        if endStream then
+          return {
+            headers := if headersSent then #[] else respHeaders
+            body := ← encodeManyIO msgs respAlg
+            trailers := Metadata.statusHeaders st
+            finished := true
+          }
+        else
+          return {
+            headers := if headersSent then #[] else respHeaders
+            body := ← encodeManyIO msgs respAlg
+            finished := false
+          }
 
 def serveH2c (s : Server) (cfg : H2.ServerConfig := {}) : IO Unit :=
   H2.Server.listen cfg (handlerFor s none false)

Grpc/Stream.lean

@@ -10,6 +10,7 @@ import Hpack
 import Grpc.Status
 import Grpc.Message
 import Grpc.Metadata
+import Grpc.PeerIdentity
 import Grpc.Client
 
 namespace Grpc.Stream
@@ -219,6 +220,24 @@ abbrev ClientStreamHandler := Array ByteArray → IO (ByteArray × Status)
 /-- Bidi handler: many requests → many responses (buffered batch for now). -/
 abbrev BidiStreamHandler := Array ByteArray → IO (Array ByteArray × Status)
 
+/-! ## Context-aware streaming handler types (mTLS IAM parity, v1.5.0)
+
+Each variant receives a `Grpc.StreamCallContext` (alias for `ServerCallContext`)
+carrying mTLS `peerIdentity` + inbound request metadata, matching the contract
+already available to unary handlers via `UnaryHandlerWithContext`. -/
+
+/-- Server streaming handler with `StreamCallContext` (peer identity + metadata). -/
+abbrev ServerStreamHandlerWithContext :=
+  Grpc.StreamCallContext → ByteArray → IO (Array ByteArray × Status)
+
+/-- Client streaming handler with `StreamCallContext`. -/
+abbrev ClientStreamHandlerWithContext :=
+  Grpc.StreamCallContext → Array ByteArray → IO (ByteArray × Status)
+
+/-- Bidi streaming handler with `StreamCallContext`. -/
+abbrev BidiStreamHandlerWithContext :=
+  Grpc.StreamCallContext → Array ByteArray → IO (Array ByteArray × Status)
+
 structure Incoming where
   messages : Array ByteArray
   deriving Inhabited