v1.3.0: Off-loop TLS (#10)

.github/workflows/ci.yml

@@ -22,7 +22,7 @@ jobs:
           chmod +x scripts/fetch-openssl-headers.sh
           ./scripts/fetch-openssl-headers.sh
       - name: Build libraries and tests
-        run: lake build Proofs bytesTests hpackTests h2Tests grpcTests securityTests trailersServer trailersLoopback asyncH2cLoopback tlsServer tlsLoopback helloworldServer helloworldClient interopServer interopClient protocGenLean4Grpc benchUnary benchSoak opsSmoke h2specServer routeGuideServer routeGuideClient adcSmoke fakeAdsServer
+        run: lake build Proofs bytesTests hpackTests h2Tests grpcTests securityTests trailersServer trailersLoopback asyncH2cLoopback asyncTlsLoopback tlsServer tlsLoopback helloworldServer helloworldClient interopServer interopClient protocGenLean4Grpc benchUnary benchSoak opsSmoke h2specServer routeGuideServer routeGuideClient adcSmoke fakeAdsServer
       - name: Formal proofs (compile-time)
         run: lake build Proofs
       - name: Unit tests
@@ -34,6 +34,7 @@ jobs:
           ./.lake/build/bin/securityTests
           ./.lake/build/bin/trailersLoopback
           ./.lake/build/bin/asyncH2cLoopback
+          ./.lake/build/bin/asyncTlsLoopback
       - name: Native ASAN / UBSan security harness
         run: |
           chmod +x scripts/security-asan.sh

CHANGELOG.md

@@ -1,6 +1,18 @@
 # Changelog
 
-All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.2.0**). Git tags such as `v1.2.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.3.0**). Git tags such as `v1.3.0` are created manually by maintainers when publishing.
+
+## [1.3.0] — 2026-08-11
+
+Off-loop TLS so OpenSSL does not stall the UV loop ([#10](https://github.com/RileyBetts/lean-grpc/issues/10)).
+
+- **`H2.runOffLoop` / `AsyncByteTransport.ofBlockingOffLoop`:** blocking `IO` (including `SSL_*`) runs on `IO.asTask .dedicated`, then resumes Async — UV stays free.
+- **Async TLS APIs:** `Tls.connectH2Async`, `Tls.serveH2Async`, `Server.serveTlsAsync`. Sync `connectH2` / `serveH2` / `serveTls` remain pure blocking `IO` (safe under `IO.asTask`; no nested `Async.block`).
+- **Honesty:** still **blocking** OpenSSL FFI — documented as off-loop, not nonblocking BIO.
+- **Tests:** `asyncTlsLoopback` — concurrent off-loop TLS clients + Async h2c on one UV loop; in-process `serveTlsAsync` smoke.
+- **Docs:** [docs/async-io.md](docs/async-io.md) updated for the v1.3.0 TLS model.
+
+Migration: additive — bump pin to `v1.3.0`. Prefer `*Async` TLS under Async composition; keep IO APIs for lean-compliance.
 
 ## [1.2.0] — 2026-08-11
 

Grpc.lean

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

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.2.0") : Hpack.HeaderField :=
+def userAgent (version : String := "1.3.0") : Hpack.HeaderField :=
   ⟨ascii "user-agent", ascii s!"grpc-lean/{version}"⟩
 
 def http415 : Array Hpack.HeaderField :=

Grpc/Server.lean

@@ -315,10 +315,15 @@ def serveH2cAsync (s : Server) (cfg : H2.ServerConfig := {}) : Async Unit :=
 /-- Serve with in-process TLS+ALPN `h2` (see `Grpc.Tls.serveH2` for the
     plaintext/mTLS decision based on `tlsCfg`). Peer identity is extracted per
     accepted connection and threaded into unary context handlers.
-    TLS byte IO remains blocking OpenSSL FFI in v1.2.0 — see docs/async-io.md. -/
+    OpenSSL stays blocking FFI but runs **off** the UV loop in v1.3.0 — see docs/async-io.md. -/
 def serveTls (s : Server) (tlsCfg : Tls.Config) (cfg : H2.ServerConfig := {}) : IO Unit :=
   let mtlsRequired := tlsCfg.clientCaPath.isSome
   Tls.serveH2 tlsCfg cfg fun peerId => handlerFor s peerId mtlsRequired
 
+/-- Async TLS serve: accept/handshake/`SSL_*` off-loop; connections on `background`. -/
+def serveTlsAsync (s : Server) (tlsCfg : Tls.Config) (cfg : H2.ServerConfig := {}) : Async Unit :=
+  let mtlsRequired := tlsCfg.clientCaPath.isSome
+  Tls.serveH2Async tlsCfg cfg fun peerId => handlerFor s peerId mtlsRequired
+
 end Server
 end Grpc

Grpc/Tls.lean

@@ -6,6 +6,9 @@ import H2
 import Grpc.Resolver
 import Grpc.Native.Tls
 import Grpc.PeerIdentity
+import Std.Async
+
+open Std.Async
 
 namespace Grpc.Tls
 
@@ -33,10 +36,21 @@ structure Config where
 def envoySidecarNotes : String :=
   "Optional: terminate TLS at Envoy/Caddy with alpn_protocols: [h2], cluster to 127.0.0.1:<lean-h2c-port>."
 
-/-- Connect with TLS+ALPN `h2`.
+/-- In-process OpenSSL dial (blocking). Used by sync `connectH2`. -/
+private def dialInProcess (host : String) (port : UInt16) (cfg : Config) : IO H2.ClientConn := do
+  if cfg.insecureSkipVerify then
+    IO.eprintln "WARN: Tls.Config.insecureSkipVerify=true → peer certificate not verified"
+  let ca := (cfg.caPath.map (·.toString)).getD ""
+  let sni := cfg.serverName.getD host
+  let clientCert := (cfg.certPath.map (·.toString)).getD ""
+  let clientKey := (cfg.keyPath.map (·.toString)).getD ""
+  let conn ← Grpc.Native.Tls.dial host port ca sni clientCert clientKey cfg.insecureSkipVerify
+  H2.Client.connectTransport (Grpc.Native.Tls.transport conn)
+
+/-- Connect with TLS+ALPN `h2` (blocking `IO`; safe under `IO.asTask`).
     Priority:
     1. `LEAN_GRPC_TLS_PROXY` — h2c to local sidecar/proxy (legacy).
-    2. In-process OpenSSL (system CA / `caPath` + hostname verify unless `insecureSkipVerify`).
+    2. In-process OpenSSL.
     3. `LEAN_GRPC_TLS_INSECURE_FALLBACK=1` — plain h2c (dev only). -/
 def connectH2 (host : String) (port : UInt16) (cfg : Config := {}) : IO H2.ClientConn := do
   if let some proxy := ← IO.getEnv "LEAN_GRPC_TLS_PROXY" then
@@ -48,21 +62,66 @@ def connectH2 (host : String) (port : UInt16) (cfg : Config := {}) : IO H2.Clien
     IO.eprintln "WARN: LEAN_GRPC_TLS_INSECURE_FALLBACK=1 → h2c (no TLS)"
     H2.Client.connectH2c host port
   | _ =>
+    dialInProcess host port cfg
+
+/-- Connect with TLS+ALPN `h2` under `Std.Async` (off-loop OpenSSL).
+    Blocking dial/handshake/preface run on dedicated threads — not nonblocking BIO. -/
+def connectH2Async (host : String) (port : UInt16) (cfg : Config := {}) : Async H2.ClientConn := do
+  if let some proxy := ← IO.getEnv "LEAN_GRPC_TLS_PROXY" then
+    let addr ← IO.ofExcept (Resolver.parseTarget proxy)
+    IO.eprintln s!"Tls.connectH2Async via LEAN_GRPC_TLS_PROXY={proxy} (ALPN terminated externally)"
+    return (← H2.Client.connectH2cAsync addr.host addr.port)
+  match ← IO.getEnv "LEAN_GRPC_TLS_INSECURE_FALLBACK" with
+  | some "1" =>
+    IO.eprintln "WARN: LEAN_GRPC_TLS_INSECURE_FALLBACK=1 → h2c (no TLS)"
+    H2.Client.connectH2cAsync host port
+  | _ => do
     if cfg.insecureSkipVerify then
       IO.eprintln "WARN: Tls.Config.insecureSkipVerify=true → peer certificate not verified"
     let ca := (cfg.caPath.map (·.toString)).getD ""
     let sni := cfg.serverName.getD host
     let clientCert := (cfg.certPath.map (·.toString)).getD ""
     let clientKey := (cfg.keyPath.map (·.toString)).getD ""
-    let conn ← Grpc.Native.Tls.dial host port ca sni clientCert clientKey cfg.insecureSkipVerify
-    H2.Client.connectTransport (Grpc.Native.Tls.transport conn)
+    let conn ← H2.runOffLoop
+      (Grpc.Native.Tls.dial host port ca sni clientCert clientKey cfg.insecureSkipVerify)
+    H2.Client.connectTransportOffLoopAsync (Grpc.Native.Tls.transport conn)
 
-/-- Serve with in-process TLS+ALPN when cert/key are set; otherwise h2c (+ optional sidecar).
-    TLS listen binds loopback only (see native `INADDR_LOOPBACK`).
+/-- Serve with in-process TLS+ALPN under `Std.Async`. Accept/handshake run off-loop;
+    each connection is a dedicated background fiber with blocking SSL I/O. -/
+partial def serveH2Async (cfg : Config) (h2cfg : H2.ServerConfig)
+    (mkHandler : Option PeerIdentity → H2.StreamHandler) : Async Unit := do
+  match cfg.certPath, cfg.keyPath with
+  | some cert, some key =>
+    let clientCa := (cfg.clientCaPath.map (·.toString)).getD ""
+    let listener ← H2.runOffLoop
+      (Grpc.Native.Tls.listen h2cfg.port cert.toString key.toString clientCa)
+    let mtlsNote := if cfg.clientCaPath.isSome then " (mTLS: client cert required)" else ""
+    IO.println s!"H2 TLS+ALPN listening on 127.0.0.1:{h2cfg.port}{mtlsNote} (Async off-loop)"
+    while true do
+      let acceptResult ←
+        try
+          pure (Sum.inl (← H2.runOffLoop (Grpc.Native.Tls.accept listener)))
+        catch e =>
+          pure (Sum.inr e)
+      match acceptResult with
+      | .inr e =>
+        IO.eprintln s!"tls accept error: {e}"
+      | .inl conn =>
+        let peerId ← H2.runOffLoop (Grpc.Native.Tls.peerIdentity? conn)
+        background (prio := Task.Priority.dedicated) do
+          try
+            liftM (H2.serveTransport (Grpc.Native.Tls.transport conn) (mkHandler peerId))
+          catch e =>
+            IO.eprintln s!"tls conn error: {e}"
+  | _, _ =>
+    match ← IO.getEnv "LEAN_GRPC_TLS_INSECURE_FALLBACK" with
+    | some "1" => H2.Server.listenAsync h2cfg (mkHandler none)
+    | _ =>
+      IO.eprintln s!"Tls.serveH2Async: serving h2c on {h2cfg.host}:{h2cfg.port}; set certPath/keyPath for in-process TLS, or use sidecar. {envoySidecarNotes}"
+      H2.Server.listenAsync h2cfg (mkHandler none)
 
-    `mkHandler` receives the verified peer identity for each accepted connection
-    (`none` when the client presented no certificate). Failed accepts/handshakes
-    are logged and the listen loop continues. -/
+/-- Serve with in-process TLS+ALPN (blocking `IO` accept loop; per-conn `IO.asTask`).
+    Does not go through `Async.block` — safe when the process is dedicated to serving. -/
 partial def serveH2 (cfg : Config) (h2cfg : H2.ServerConfig)
     (mkHandler : Option PeerIdentity → H2.StreamHandler) : IO Unit := do
   match cfg.certPath, cfg.keyPath with

H2/Client.lean

@@ -89,10 +89,18 @@ def connectTransportAsync (t : AsyncByteTransport) : Async ClientConn := do
   readBuf.set buf
   return { transport := t, state, readBuf }
 
-/-- Sync/TLS entry: wrap blocking `ByteTransport` then run async preface exchange. -/
+/-- Sync/TLS entry: wrap blocking `ByteTransport` then run async preface via `.block`.
+    Prefer calling this from an off-loop dedicated task (`H2.runOffLoop`) so OpenSSL
+    does not stall the UV thread. -/
 def connectTransport (t : ByteTransport) : IO ClientConn :=
   (connectTransportAsync (.ofBlocking t)).block
 
+/-- Dial/preface on a dedicated thread (blocking OpenSSL), then return a `ClientConn`
+    whose later Async send/recv use `ofBlockingOffLoop` (issue #10). -/
+def connectTransportOffLoopAsync (t : ByteTransport) : Async ClientConn := do
+  let c ← runOffLoop (connectTransport t)
+  pure { c with transport := .ofBlockingOffLoop t }
+
 /-- Dial h2c without `.block` on connect/send/recv. -/
 def connectH2cAsync (host : String) (port : UInt16) : Async ClientConn := do
   let sock ← TCP.Socket.Client.mk

H2/Transport.lean

@@ -28,12 +28,25 @@ def tcpTransportAsync (sock : TCP.Socket.Client) : AsyncByteTransport where
   close := pure ()
 
 /-- Lift blocking `IO` send/recv into `Async` (still blocks the UV thread while
-    the IO runs — used for OpenSSL FFI transports in v1.2.0). -/
+    the IO runs). Prefer `ofBlockingOffLoop` for OpenSSL / other blocking FFI. -/
 def AsyncByteTransport.ofBlocking (t : ByteTransport) : AsyncByteTransport where
   send := fun b => liftM (t.send b)
   recv? := fun n => liftM (t.recv? n)
   close := liftM t.close
 
+/-- Run blocking `IO` on a dedicated thread, then resume the Async waiter.
+    Keeps `SSL_read` / `SSL_write` / similar FFI off the UV loop (issue #10). -/
+def runOffLoop (act : IO α) (prio := Task.Priority.dedicated) : Async α := do
+  let t ← IO.asTask act prio
+  Async.ofAsyncTask t
+
+/-- Lift blocking `IO` send/recv into `Async` without stalling the UV loop:
+    each op runs on a dedicated task (off-loop OpenSSL model for v1.3.0). -/
+def AsyncByteTransport.ofBlockingOffLoop (t : ByteTransport) : AsyncByteTransport where
+  send := fun b => runOffLoop (t.send b)
+  recv? := fun n => runOffLoop (t.recv? n)
+  close := runOffLoop t.close
+
 /-- Sync facade: each op `.block`s the underlying async transport. -/
 def ByteTransport.ofAsync (t : AsyncByteTransport) : ByteTransport where
   send := fun b => (t.send b).block

README.md

@@ -6,9 +6,9 @@
 
 General-purpose **Lean 4 gRPC library**: HPACK + HTTP/2 + gRPC framing over `Std.Async.TCP`.
 
-Standalone Lake package (**1.2.0**). Consumers depend via git tag or, after indexing, [Reservoir](https://reservoir.lean-lang.org/).
+Standalone Lake package (**1.3.0**). Consumers depend via git tag or, after indexing, [Reservoir](https://reservoir.lean-lang.org/).
 
-**Async model:** sockets are `Std.Async.TCP`. Through v1.1.x the public API was blocking `IO` via `.block`. **v1.2.0** adds a native Async h2c path (`serveH2cAsync` / `unaryAsync`) with **zero** `.block` on accept/connect/send/recv; existing IO APIs remain as explicit sync adapters. In-process TLS is still blocking OpenSSL FFI — see [docs/async-io.md](docs/async-io.md).
+**Async model:** sockets are `Std.Async.TCP`. **v1.2.0** added a native Async h2c path (`serveH2cAsync` / `unaryAsync`) with **zero** `.block` on accept/connect/send/recv. **v1.3.0** runs blocking OpenSSL on dedicated threads (`connectH2Async` / `serveTlsAsync` / `ofBlockingOffLoop`) so TLS does not stall the UV loop — still not nonblocking BIO; see [docs/async-io.md](docs/async-io.md).
 
 **Docs:** [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc) (curated) · [docs/](docs/README.md) (full in-repo index)
 
@@ -22,7 +22,7 @@ In your `lakefile.lean`:
 
 ```lean
 require «lean-grpc» from git
-  "https://github.com/RileyBetts/lean-grpc.git" @ "v1.2.0"
+  "https://github.com/RileyBetts/lean-grpc.git" @ "v1.3.0"
 ```
 
 Then `import Grpc`. After Reservoir lists the package you can use `require «lean-grpc»` without a git URL. Packaging details and the maintainer release checklist: [docs/packaging.md](docs/packaging.md).

ROADMAP.md

@@ -1,6 +1,6 @@
 # Roadmap
 
-lean-grpc **v1.2.0** is the current package tip (Lake / `Grpc.version`): an interop-tested Lean 4 gRPC stack with native Async h2c APIs (honest Std.Async model), a CI-gated **`Proofs`** library for selected pure codecs, plus additive mTLS peer-identity / request-context APIs for enterprise AuthN. It is **not** a machine-checked end-to-end PROTOCOL-HTTP2 / TLS / session proof.
+lean-grpc **v1.3.0** is the current package tip (Lake / `Grpc.version`): an interop-tested Lean 4 gRPC stack with native Async h2c APIs, **off-loop** in-process TLS (blocking OpenSSL on dedicated threads), a CI-gated **`Proofs`** library for selected pure codecs, plus additive mTLS peer-identity / request-context APIs for enterprise AuthN. It is **not** a machine-checked end-to-end PROTOCOL-HTTP2 / TLS / session proof.
 
 This document records what shipped, what is still open, and the next proof/hardening tranches.
 
@@ -25,13 +25,23 @@ First public packaging baseline (interop + Lake/Reservoir layout). Formal Lean p
 | Dial / LB / retry, health, reflection, channelz | Present; ops demos gated |
 | ADC / xDS ADS | Mock / FakeAds CI; live Google paths allowlisted |
 
+## Shipped — v1.3.0 (TLS off-loop)
+
+Blocking OpenSSL runs off the UV loop ([#10](https://github.com/RileyBetts/lean-grpc/issues/10), [docs/async-io.md](docs/async-io.md)).
+
+| Included | Deferred |
+|---|---|
+| `runOffLoop` / `ofBlockingOffLoop` | Nonblocking BIO / `SSL_ERROR_WANT_*` + UV readiness |
+| `connectH2Async` / `serveTlsAsync` | Streaming `*Async` surface beyond unary |
+| `asyncTlsLoopback` CI (TLS + h2c concurrent) | Full Concurrent retry/hedge under Async TLS |
+
 ## Shipped — v1.2.0 (Async honesty)
 
 Native Async h2c + docs that match the implementation ([#6](https://github.com/RileyBetts/lean-grpc/issues/6), [docs/async-io.md](docs/async-io.md)).
 
 | Included | Deferred |
 |---|---|
-| `AsyncByteTransport` / `*Async` h2c serve/dial/unary | Nonblocking TLS BIO / off-loop OpenSSL |
+| `AsyncByteTransport` / `*Async` h2c serve/dial/unary | Streaming `*Async` beyond unary; Concurrent retry/hedge under Async |
 | Sync IO APIs as `.block` adapters | Streaming `*Async` surface beyond unary |
 | Concurrent `asyncH2cLoopback` CI | Full Concurrent retry/hedge under Async |
 
@@ -109,11 +119,11 @@ Close remaining audit follow-ups so later minors are not “proved but soft”:
 ## Milestone sketch
 
 ```text
-v0.5.0 ──► v1.0.0              ──► v1.1.0              ──► v1.2.0              ──► v1.3.x
- shipped     interop +           mTLS peer identity +   Async h2c honesty     ConnState +
-             selected Proofs     ServerCallContext      (#6) + sync adapters   general frame/msg
-             (CI) + provenance   (unary IAM)                                  roundtrips /
-                                                                              Huffman trie
+v0.5.0 ──► v1.0.0              ──► v1.1.0              ──► v1.2.0              ──► v1.3.0              ──► later 1.x
+ shipped     interop +           mTLS peer identity +   Async h2c honesty     TLS off-loop (#10)    ConnState +
+             selected Proofs     ServerCallContext      (#6) + sync adapters   + serveTlsAsync       general frame/msg
+             (CI) + provenance   (unary IAM)                                                        roundtrips /
+                                                                                                    Huffman trie
 ```
 
 Dates are intentionally omitted; order matters more than calendar.