From 686e90ae369980c8780383fb98b37cf0ff353f36 Mon Sep 17 00:00:00 2001 From: Robert Betts Date: Tue, 11 Aug 2026 23:06:48 +0100 Subject: [PATCH] Add off-loop TLS so OpenSSL does not stall the UV loop (#10). Expose connectH2Async/serveTlsAsync with dedicated-thread SSL I/O, keep sync IO paths for safe composition, and ship asyncTlsLoopback + v1.3.0 docs. Co-authored-by: Cursor --- .github/workflows/ci.yml | 3 +- CHANGELOG.md | 14 +++- Grpc.lean | 2 +- Grpc/Metadata.lean | 2 +- Grpc/Server.lean | 7 +- Grpc/Tls.lean | 77 +++++++++++++++++--- H2/Client.lean | 10 ++- H2/Transport.lean | 15 +++- README.md | 6 +- ROADMAP.md | 24 +++++-- Tests/AsyncTlsLoopback.lean | 139 ++++++++++++++++++++++++++++++++++++ docs/README.md | 2 +- docs/api-reference.md | 4 +- docs/architecture.md | 5 +- docs/async-io.md | 49 +++++++------ docs/getting-started.md | 6 +- docs/packaging.md | 8 +-- lakefile.lean | 7 +- 18 files changed, 320 insertions(+), 60 deletions(-) create mode 100644 Tests/AsyncTlsLoopback.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b37a057..d639ba4 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 501bc89..4edd73e 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Grpc.lean b/Grpc.lean index 91c88b5..a7dd9d8 100644 --- a/Grpc.lean +++ b/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 diff --git a/Grpc/Metadata.lean b/Grpc/Metadata.lean index 08b591f..f57cf4e 100644 --- a/Grpc/Metadata.lean +++ b/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 := diff --git a/Grpc/Server.lean b/Grpc/Server.lean index 4d3d5d1..7f11168 100644 --- a/Grpc/Server.lean +++ b/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 diff --git a/Grpc/Tls.lean b/Grpc/Tls.lean index ad40a6c..c6979da 100644 --- a/Grpc/Tls.lean +++ b/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:." -/-- 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 diff --git a/H2/Client.lean b/H2/Client.lean index 6b60382..4b099a4 100644 --- a/H2/Client.lean +++ b/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 diff --git a/H2/Transport.lean b/H2/Transport.lean index d6b23ee..3747fdd 100644 --- a/H2/Transport.lean +++ b/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 diff --git a/README.md b/README.md index 6ff150f..985574c 100644 --- a/README.md +++ b/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). diff --git a/ROADMAP.md b/ROADMAP.md index 2346135..63f7582 100644 --- a/ROADMAP.md +++ b/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. diff --git a/Tests/AsyncTlsLoopback.lean b/Tests/AsyncTlsLoopback.lean new file mode 100644 index 0000000..f8fb733 --- /dev/null +++ b/Tests/AsyncTlsLoopback.lean @@ -0,0 +1,139 @@ +/- +Copyright © 2026, Riley Betts Ltd (rileybetts.ai) +Released under Apache 2.0 license as described in the file LICENSE. +-/ +import Grpc +import H2 +import Proto +import Std.Async +import Std.Async.Timer + +open Std.Async + +/-- Concurrent off-loop TLS clients + Async h2c on one UV loop (issue #10). + TLS server runs in a subprocess (`tlsServer`); clients use `H2.runOffLoop` so + OpenSSL cannot stall the UV loop while h2c clients progress. + Skips if `openssl` is unavailable. -/ + +private def run (cmd : String) (args : Array String) : IO Unit := do + let out ← IO.Process.output { cmd, args } + if out.exitCode != 0 then + throw (IO.userError s!"{cmd} {args} failed: {out.stderr}") + +private def haveOpenssl : IO Bool := do + try + let out ← IO.Process.output { cmd := "openssl", args := #["version"] } + return out.exitCode == 0 + catch _ => return false + +private def genCerts (dir : System.FilePath) : IO Unit := do + IO.FS.createDirAll dir + let d := dir.toString + run "openssl" #["genrsa", "-out", s!"{d}/ca.key", "2048"] + run "openssl" #["req", "-x509", "-new", "-nodes", "-key", s!"{d}/ca.key", "-sha256", + "-days", "3650", "-out", s!"{d}/ca.crt", "-subj", "/CN=LeanGrpcAsyncTlsCA"] + run "openssl" #["genrsa", "-out", s!"{d}/server.key", "2048"] + run "openssl" #["req", "-new", "-key", s!"{d}/server.key", "-out", s!"{d}/server.csr", + "-subj", "/CN=127.0.0.1"] + run "openssl" #["x509", "-req", "-in", s!"{d}/server.csr", "-CA", s!"{d}/ca.crt", + "-CAkey", s!"{d}/ca.key", "-CAcreateserial", "-out", s!"{d}/server.crt", + "-days", "825", "-sha256"] + +private def spawnTlsServer (binDir dir : System.FilePath) (port : UInt16) : + IO (IO.Process.Child {}) := do + let d := dir.toString + IO.Process.spawn { + cmd := (binDir / "tlsServer").toString + env := #[ + ("GRPC_PORT", some (toString port.toNat)), + ("TLS_CERT", some s!"{d}/server.crt"), + ("TLS_KEY", some s!"{d}/server.key") + ] + } + +/-- Blocking EmptyCall with connect retries (server spawn race). -/ +private partial def tlsEmptyIO (port : UInt16) (ca : System.FilePath) (tag : String) + (attempts : Nat := 12) : IO String := do + let cfg : Grpc.Tls.Config := { + caPath := some ca + serverName := some "127.0.0.1" + } + try + let c ← Grpc.Tls.connectH2 "127.0.0.1" port cfg + let res ← Grpc.Client.unaryCall c "grpc.testing.TestService" "EmptyCall" "127.0.0.1" + ByteArray.empty (useHttps := true) + if res.status.code != .ok then + throw (IO.userError s!"tls empty status {res.status.code.toUInt32} tag={tag}") + match String.fromUTF8? res.message with + | some s => pure s!"{tag}:{s}" + | none => throw (IO.userError "non-utf8") + catch e => + if attempts ≤ 1 then throw e + IO.sleep 250 + tlsEmptyIO port ca tag (attempts - 1) + +/-- Off-loop TLS EmptyCall client. -/ +private def tlsEmptyClient (port : UInt16) (ca : System.FilePath) (tag : String) : Async String := + H2.runOffLoop (tlsEmptyIO port ca tag) + +private def h2cClient (port : UInt16) (name : String) : Async String := do + let c ← H2.Client.connectH2cAsync "127.0.0.1" port + let req := Proto.HelloRequest.encode { name } + let res ← Grpc.Client.unaryCallAsync c "helloworld.Greeter" "SayHello" "127.0.0.1" req + if res.status.code != .ok then + throw (IO.userError s!"h2c status {res.status.code.toUInt32}") + let reply ← liftM (IO.ofExcept (Proto.HelloReply.decode res.message)) + return reply.message + +def main : IO Unit := do + if !(← haveOpenssl) then + IO.println "asyncTlsLoopback SKIPPED (no openssl)" + return + let dir := (← IO.currentDir) / ".lake" / "build" / "async-tls-loopback-certs" + genCerts dir + let binDir ← IO.appDir + let tlsPort : UInt16 := 50071 + let h2cPort : UInt16 := 50072 + let mut s := Grpc.Server.empty + s := Grpc.Server.register s "helloworld.Greeter" "SayHello" fun reqBytes => do + let req ← IO.ofExcept (Proto.HelloRequest.decode reqBytes) + let reply : Proto.HelloReply := { message := s!"Hello, {req.name}" } + return (Proto.HelloReply.encode reply, Grpc.Status.ok) + let srv ← spawnTlsServer binDir dir tlsPort + try + (do + background (prio := Task.Priority.dedicated) do + Grpc.Server.serveH2cAsync s { host := "127.0.0.1", port := h2cPort } + sleep (Std.Time.Millisecond.Offset.ofNat 600) + let tlsTags : Array String := #["T1", "T2", "T3", "T4"] + let h2cNames : Array String := #["H1", "H2", "H3", "H4"] + let tlsJobs := tlsTags.map (fun t => tlsEmptyClient tlsPort (dir / "ca.crt") t) + let h2cJobs := h2cNames.map (fun n => h2cClient h2cPort n) + let msgs ← Async.concurrentlyAll (tlsJobs ++ h2cJobs) + if msgs.size != tlsTags.size + h2cNames.size then + throw (IO.userError s!"expected {tlsTags.size + h2cNames.size} replies, got {msgs.size}") + for msg in msgs do + if !("T".isPrefixOf msg || "Hello".isPrefixOf msg) then + throw (IO.userError msg) + -- Phase 2: in-process `serveTlsAsync` + off-loop client (same UV loop as h2c). + let asyncTlsPort : UInt16 := 50073 + let tlsCfg : Grpc.Tls.Config := { + certPath := some (dir / "server.crt") + keyPath := some (dir / "server.key") + } + let mut s2 := Grpc.Server.empty + s2 := Grpc.Server.registerWithContext s2 "grpc.testing.TestService" "EmptyCall" + fun _ _ => pure (ByteArray.empty, Grpc.Status.ok) + background (prio := Task.Priority.dedicated) do + Grpc.Server.serveTlsAsync s2 tlsCfg { host := "127.0.0.1", port := asyncTlsPort } + sleep (Std.Time.Millisecond.Offset.ofNat 400) + let body ← tlsEmptyClient asyncTlsPort (dir / "ca.crt") "ASYNC" + if !("ASYNC:".isPrefixOf body) then + throw (IO.userError body) + IO.println "asyncTlsLoopback OK" + -- Background accept loops (h2c + serveTlsAsync) keep dedicated threads alive; + -- force a clean exit so Lake/CI do not hang in task_manager finalization. + IO.Process.exit 0 + ).block + finally + srv.kill diff --git a/docs/README.md b/docs/README.md index 798533e..8770e10 100644 --- a/docs/README.md +++ b/docs/README.md @@ -22,7 +22,7 @@ User and contributor docs for the Lean 4 gRPC stack. | [Formal proofs](proofs.md) | Compile-time `Proofs` library for pure codecs / maps | | [TLS / Envoy](tls-envoy.md) | In-process OpenSSL and optional sidecars | | [CHANGELOG](../CHANGELOG.md) | Package version history | -| [ROADMAP](../ROADMAP.md) | What v1.2.0 shipped vs open proof/hardening follow-ups | +| [ROADMAP](../ROADMAP.md) | What v1.3.0 shipped vs open proof/hardening follow-ups | | [CONTRIBUTING](../CONTRIBUTING.md) | Dev setup, tests, PR expectations | | [SECURITY](../SECURITY.md) | Vulnerability reporting | | [Code of Conduct](../CODE_OF_CONDUCT.md) | Community standards | diff --git a/docs/api-reference.md b/docs/api-reference.md index 88a1f2c..c8603c4 100644 --- a/docs/api-reference.md +++ b/docs/api-reference.md @@ -1,6 +1,6 @@ # API reference -Lean module catalogue for consumers. Signatures are summarized; see source under `Grpc/`, `H2/`, `Proto/` for full definitions. Version string: `Grpc.version` (currently `1.2.0`). Async vs sync IO: [async-io.md](async-io.md). +Lean module catalogue for consumers. Signatures are summarized; see source under `Grpc/`, `H2/`, `Proto/` for full definitions. Version string: `Grpc.version` (currently `1.3.0`). Async vs sync IO: [async-io.md](async-io.md). Import umbrella: `import Grpc` (pulls status, channel, server, credentials, TLS, xDS, ops, etc.). Add `import Proto` for bundled message codecs. @@ -122,7 +122,7 @@ Verified mTLS peer certificate identity (OpenSSL; subject DN is **RFC 2253**): | `registerServerStream` / `registerClientStream` / `registerBidi` | Streaming (raw bytes; context deferred) | | `registerServerStreamTyped` / `registerClientStreamTyped` / `registerBidiTyped` | Streaming with decode/encode adapters | | `serveH2c` / `serveH2cAsync` | Listen h2c (`peerIdentity = none`); Async path has no `.block` on accept/send/recv | -| `serveTls` | Listen TLS+ALPN; per-connection peer identity → context handlers (**blocking** OpenSSL FFI in v1.2.0) | +| `serveTls` / `serveTlsAsync` | Listen TLS+ALPN; per-connection peer identity → context handlers (OpenSSL **off-loop** under Async in v1.3.0) | | `maxMsgSize` | Inbound limit | Bad `content-type` → HTTP **415**. Unknown method / zero timeout → trailers-only gRPC status. diff --git a/docs/architecture.md b/docs/architecture.md index 81f479c..1eef5f8 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -61,7 +61,7 @@ Health, reflection, and channelz are ordinary registered methods (`Grpc.Health`, - Plain TCP Async (`H2.Client.connectH2cAsync`, `H2.Server.listenH2cAsync`) — **no** `.block` on the Async chain - Plain TCP sync adapters (`connectH2c`, `listenH2c`) — `.block` at the edge -- In-process OpenSSL ALPN `h2` (`Grpc.Native.Tls` → `Tls.connectH2` / `serveH2`) — **blocking FFI** in v1.2.0; see [async-io.md](async-io.md) +- In-process OpenSSL ALPN `h2` (`Grpc.Native.Tls` → `Tls.connectH2` / `serveH2` / `*Async`) — **blocking FFI**, **off-loop** under Async in v1.3.0; see [async-io.md](async-io.md) - Optional sidecar via `LEAN_GRPC_TLS_PROXY` (client dials h2c to a local terminator) ## Credentials @@ -104,7 +104,8 @@ These are intentionally lightweight compared to full OpenTelemetry SDKs. ## Process / concurrency model - Networking uses Lean 4 `Std.Async` (libuv-backed). Prefer one event-loop owner per process for listen/accept. -- **v1.2.0+:** `serveH2cAsync` schedules connections with `Std.Async.background` so concurrent h2c clients can share one UV loop. See [async-io.md](async-io.md). +- **v1.2.0+:** `serveH2cAsync` schedules connections with `Std.Async.background` so concurrent h2c clients can share one UV loop. +- **v1.3.0+:** TLS accept/handshake/`SSL_*` run via `H2.runOffLoop` / dedicated fibers so OpenSSL does not stall that loop. See [async-io.md](async-io.md). - Interop loopbacks that need a second peer may still **spawn a child executable** (e.g. `trailersLoopback`) when mixing sync `.block` adapters with tasks. - CI runs multi-language peers as separate processes (Go / Python / h2spec). diff --git a/docs/async-io.md b/docs/async-io.md index 9994f25..1a87360 100644 --- a/docs/async-io.md +++ b/docs/async-io.md @@ -1,4 +1,4 @@ -# Async IO model (v1.2.0) +# Async IO model (v1.3.0) lean-grpc uses Lean 4 `Std.Async.TCP` (libuv-backed) for sockets. Through **v1.1.x** the public API collapsed every accept/connect/send/recv with @@ -6,7 +6,7 @@ lean-grpc uses Lean 4 `Std.Async.TCP` (libuv-backed) for sockets. Through constructors. That overstated “runs on Std.Async” — see [GitHub #6](https://github.com/RileyBetts/lean-grpc/issues/6). -## v1.2.0 model +## v1.2.0+ h2c model | Layer | Behavior | |---|---| @@ -14,39 +14,48 @@ constructors. That overstated “runs on Std.Async” — see | `H2.listenH2cAsync` / `connectH2cAsync` / `awaitResponseAsync` | Async accept/dial/RPC wait | | `Grpc.Server.serveH2cAsync` / `Channel.unaryAsync` | Additive Async gRPC entry points | | `ByteTransport` / `serveH2c` / `unary` / `connectH2c` | **Sync adapters** — `.block` at the edge only | -| In-process TLS (`SSL_read` / `SSL_write`) | Still **blocking FFI**; wrapped via `AsyncByteTransport.ofBlocking` | + +## v1.3.0 TLS off-loop model + +In-process OpenSSL (`SSL_read` / `SSL_write` / handshake) remains **blocking FFI**. +**v1.3.0** runs that FFI on **dedicated threads** so the UV loop is not stalled +([#10](https://github.com/RileyBetts/lean-grpc/issues/10)): + +| Layer | Behavior | +|---|---| +| `H2.runOffLoop` / `AsyncByteTransport.ofBlockingOffLoop` | `IO.asTask .dedicated` + await — SSL off UV | +| `Tls.connectH2Async` / `serveH2Async` / `Server.serveTlsAsync` | Accept/handshake off-loop; conns on `background` | +| `Tls.connectH2` / `serveH2` / `serveTls` | Blocking `IO` (safe under `IO.asTask`; no nested `Async.block`) | + +This is **off-loop blocking TLS**, not nonblocking BIO. Do not claim “fully async +OpenSSL” until a BIO/`WANT_READ` integration lands (follow-up issue). ```text - App (Async) ──► serveH2cAsync / unaryAsync + App (Async) ──► serveH2cAsync / unaryAsync (h2c, zero .block) + └─► serveTlsAsync / connectH2Async (TLS off-loop) │ ▼ - AsyncByteTransport (TCP) ← zero .block on h2c hot path + dedicated Task ──► SSL_* (blocking FFI) │ - ▼ - Std.Async.TCP + UV loop + UV loop stays free for Std.Async.TCP - App (IO) ──► serveH2c / unary ──► (asyncPath).block ← explicit adapter + App (IO) ──► serveTls / connectH2 (plain blocking IO accept/dial) ``` ## UV loop ownership Prefer **one** event-loop owner per process. Nested `.block` inside -`IO.asTask` workers on the same loop is fragile (historical -`TrailersLoopback` note). The Async listen path schedules connections with -`Std.Async.background` instead. - -## TLS caveat (v1.2.0) - -OpenSSL in `native/tls_ffi.c` is blocking. `serveTls` / `connectH2` remain -correct and tested, but they are **not** end-to-end async. Do not claim TLS is -async until a nonblocking BIO or off-loop worker pool lands (follow-up issue). +`IO.asTask` / `runOffLoop` workers is fragile (historical `TrailersLoopback` +note). Use pure `IO` for sync TLS helpers when already on a dedicated thread; +use `Std.Async.background` for connection scheduling under Async. ## Migration | Need | Use | |---|---| | Compose without blocking the loop (h2c) | `*Async` APIs | -| Existing code / lean-compliance | Keep `IO` APIs (adapters) | -| mTLS AuthN | `serveTls` + `registerWithContext` (sync FFI underneath) | +| Compose under Async without freezing UV (TLS) | `connectH2Async` / `serveTlsAsync` / `runOffLoop` | +| Existing code / lean-compliance | Keep `IO` APIs | +| mTLS AuthN | `serveTls` or `serveTlsAsync` + `registerWithContext` | -Pin: `@ "v1.2.0"`. +Pin: `@ "v1.3.0"`. diff --git a/docs/getting-started.md b/docs/getting-started.md index 9a8f760..bec329b 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -4,7 +4,7 @@ This guide gets a Lean 4 unary gRPC server and client running on h2c with **type **Requirements:** Lean 4.32+ (see `lean-toolchain`), OpenSSL headers for the `Grpc` library (`libssl-dev` or `./scripts/fetch-openssl-headers.sh`). Peer gzip optionally uses a zlib helper (`./scripts/build_native.sh`) or system `gzip`. -Package version: **1.2.0** (`lakefile.lean` / `Grpc.version`). +Package version: **1.3.0** (`lakefile.lean` / `Grpc.version`). ## Build the repo @@ -151,12 +151,12 @@ 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` (and `Proto` if you use the bundled codecs). Public libs: `Bytes`, `Hpack`, `H2`, `Proto`, `Grpc`. Linking OpenSSL (`-lssl -lcrypto`) is pulled in via the `Grpc` Lake library (not via Bytes/Hpack/H2 alone). For peer gzip against foreign stacks, set `LEAN_GRPC_ZLIB_HELPER` after `./scripts/build_native.sh`. Full packaging notes: [packaging.md](packaging.md). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). -After [Reservoir](https://reservoir.lean-lang.org/) indexes the package you can use `require «lean-grpc»` without a git URL. Pin a commit SHA if the `v1.2.0` tag is not yet on the remote you use. +After [Reservoir](https://reservoir.lean-lang.org/) indexes the package you can use `require «lean-grpc»` without a git URL. Pin a commit SHA if the `v1.3.0` tag is not yet on the remote you use. ## Next steps diff --git a/docs/packaging.md b/docs/packaging.md index 510c0ec..c25b9da 100644 --- a/docs/packaging.md +++ b/docs/packaging.md @@ -65,7 +65,7 @@ lake build ```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` (and `Proto` if using bundled codecs). @@ -76,7 +76,7 @@ Then `import Grpc` (and `Proto` if using bundled codecs). require «lean-grpc» -- once listed on reservoir.lean-lang.org ``` -Package version in-tree is **1.2.0** (`lakefile.lean`, `Grpc.version`). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). Creating the git tag on origin is a separate maintainer step (below). +Package version in-tree is **1.3.0** (`lakefile.lean`, `Grpc.version`). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). Creating the git tag on origin is a separate maintainer step (below). ## Maintainer release checklist @@ -89,8 +89,8 @@ Documented only — do **not** automate tagging from CI or agent runs. 5. **Manual version tagging (maintainer only):** on `main`, when you choose to publish: ```bash - git tag -a v1.2.0 -m "lean-grpc 1.2.0" - git push origin v1.2.0 + git tag -a v1.3.0 -m "lean-grpc 1.3.0" + git push origin v1.3.0 ``` Agents and CI must not create or push tags. diff --git a/lakefile.lean b/lakefile.lean index 107f53a..8b5ef3c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,9 +7,9 @@ open Lake DSL open System package «lean-grpc» where - version := v!"1.2.0" + version := v!"1.3.0" keywords := #["grpc", "http2", "hpack", "protobuf", "networking"] - description := "Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC); Std.Async.TCP with native Async h2c APIs" + description := "Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC); Async h2c + off-loop TLS" homepage := "https://rileybetts.ai/oss/lean-grpc" license := "Apache-2.0" licenseFiles := #["LICENSE", "NOTICE"] @@ -70,6 +70,9 @@ lean_exe trailersLoopback where lean_exe asyncH2cLoopback where root := `Tests.AsyncH2cLoopback +lean_exe asyncTlsLoopback where + root := `Tests.AsyncTlsLoopback + lean_exe tlsServer where root := `Tests.TlsServer