Development

CHANGELOG.md

@@ -1,6 +1,22 @@
 # Changelog
 
-All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.0.0**). Git tags such as `v1.0.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.1.0**). Git tags such as `v1.1.0` are created manually by maintainers when publishing.
+
+## [1.1.0] — 2026-08-04
+
+Additive IAM surface for enterprise mTLS AuthN (lean-compliance G1–G4).
+
+- **Peer identity:** `Grpc.Native.Tls.peerIdentity?` extracts verified client cert fields (RFC 2253 subject DN, CN, DNS/URI SANs, SHA-256 fingerprint, serial) via OpenSSL after mTLS handshake.
+- **Request context:** `ServerCallContext` + `registerWithContext` / `registerTypedWithContext` pass `peerIdentity`, inbound metadata, and `methodPath` into unary handlers. Legacy `register` remains (ignores context).
+- **TLS serve:** `Tls.serveH2` takes a per-connection handler factory; failed accepts/handshakes are logged and the listen loop continues.
+- **Interceptors:** `registerUnaryWithContext`, `requirePeerIdentity` (fail closed when `mtlsRequired` and identity missing).
+- **Tests:** `tlsLoopback` covers dual-cert identity binding, metadata non-forgery, h2c → `none`, accept-loop survival.
+- **Codegen:** `protoc-gen-lean4-grpc` emits `register{Svc}{Method}WithContext` alongside body-only registrars.
+- **Examples:** MirrorForge `Stamp` uses `registerUnaryWithContext` (Bearer metadata + body-token fallback; optional env-gated TLS/mTLS).
+- **Docs:** cookbook mTLS → `ctx.peerIdentity`; API reference; security PKI note.
+- **Deferred:** streaming handlers with context; trusted-proxy identity mode; JWT/OIDC validation inside lean-grpc.
+
+Migration: additive API — bump consumer pin from `v1.0.0` to `v1.1.0`. Prefer `registerWithContext` for AuthN; do not trust client-supplied subject metadata.
 
 ## [1.0.0] — 2026-08-02
 

Examples/Helloworld/Generated.lean

@@ -65,4 +65,10 @@ def registerGreeterSayHello (s : Grpc.Server)
       let (resp, st) ← h req
       return (HelloReply.encode resp, st)
 
+/-- Register a typed unary handler with `ServerCallContext` for `Greeter/SayHello`. -/
+def registerGreeterSayHelloWithContext (s : Grpc.Server)
+    (h : Grpc.ServerCallContext → HelloRequest → IO (HelloReply × Grpc.Status)) : Grpc.Server :=
+  Grpc.Server.registerTypedWithContext s "helloworld.Greeter" "SayHello"
+    HelloRequest.decode HelloReply.encode h
+
 end helloworld

Examples/MirrorForge/Client.lean

@@ -25,6 +25,26 @@ private def containsService (services : Array String) (name : String) : Bool :=
       if s == name then return true
     return false
 
+/-- Dial options: h2c by default; set `TLS_CA` (+ optional client `TLS_CERT`/`TLS_KEY`) for TLS/mTLS. -/
+private def dialOptions : IO Grpc.Credentials.DialOptions := do
+  match ← IO.getEnv "TLS_CA" with
+  | none => pure {}
+  | some ca =>
+      let cert := (← IO.getEnv "TLS_CERT").getD ""
+      let key := (← IO.getEnv "TLS_KEY").getD ""
+      let serverName := (← IO.getEnv "TLS_SERVER_NAME").getD "127.0.0.1"
+      let tls : Grpc.Tls.Config := {
+        caPath := some (System.FilePath.mk ca)
+        serverName := some serverName
+        certPath := if cert.isEmpty then none else some (System.FilePath.mk cert)
+        keyPath := if key.isEmpty then none else some (System.FilePath.mk key)
+      }
+      pure { channel := .tls tls }
+
+/-- Preferred Stamp credentials: Bearer metadata (body token still sent for h2c fallback demos). -/
+private def stampAuthMd : Grpc.Metadata :=
+  Grpc.Interceptor.bearerMetadata accessToken
+
 def main (args : List String) : IO UInt32 := do
   let host := args[0]?.getD "127.0.0.1"
   let portA := (args[1]?.getD "50201").toNat?.getD 50201 |>.toUInt16
@@ -41,17 +61,20 @@ def main (args : List String) : IO UInt32 := do
     if hedgeCfg.hedging.isSome then pass "act.hedge_config" "parsed"
     else fail "act.hedge_config" "missing hedgingPolicy")
 
+  let opts ← dialOptions
   IO.println "mirrorForge: dialing…"
-  let chRR ← Grpc.Channel.dial s!"dns:///{host}:{portA.toNat}" {} rrCfg
-  let chRetry ← Grpc.Channel.dial s!"{host}:{portA.toNat}" {} retryCfg
+  let chRR ← Grpc.Channel.dial s!"dns:///{host}:{portA.toNat}" opts rrCfg
+  let chRetry ← Grpc.Channel.dial s!"{host}:{portA.toNat}" opts retryCfg
   IO.println "mirrorForge: dialed"
 
-  -- Act I: interceptor-wrapped Stamp
+  -- Act I: interceptor-wrapped Stamp (Bearer metadata + body token)
   let clientLog ← IO.mkRef (#[] : Array String)
   let stampReq := StampRequest.encode { token := accessToken, billet := "ingot-1" }
   IO.println "mirrorForge: stamp_1…"
-  let stamp1 ← Grpc.Interceptor.callUnary chRR serviceName "Stamp"
-    #[Grpc.Interceptor.loggingClient clientLog] stampReq
+  let stampInvoker : Grpc.Interceptor.ClientUnaryInvoker := fun r =>
+    Grpc.Channel.unary chRR serviceName "Stamp" r stampAuthMd
+  let stamp1 ← Grpc.Interceptor.applyClient serviceName "Stamp"
+    #[Grpc.Interceptor.loggingClient clientLog] stampInvoker stampReq
   IO.println s!"mirrorForge: stamp_1 status={stamp1.status.code.toUInt32}"
   checks := checks.push (expectOk "act.stamp_1" stamp1.status.code)
   let reply1 ← IO.ofExcept (StampReply.decode stamp1.message)
@@ -67,7 +90,7 @@ def main (args : List String) : IO UInt32 := do
 
   -- Act II: round-robin across two forges
   let stamp2 ← Grpc.Channel.unary chRR serviceName "Stamp"
-    (StampRequest.encode { token := accessToken, billet := "ingot-2" })
+    (StampRequest.encode { token := accessToken, billet := "ingot-2" }) stampAuthMd
   checks := checks.push (expectOk "act.stamp_2" stamp2.status.code)
   let reply2 ← IO.ofExcept (StampReply.decode stamp2.message)
   checks := checks.push (
@@ -76,7 +99,7 @@ def main (args : List String) : IO UInt32 := do
     else
       fail "act.round_robin" s!"both hit {reply1.forgeId} (is the second forge up?)")
 
-  -- Act III: bad token → UNAUTHENTICATED
+  -- Act III: bad token → UNAUTHENTICATED (no Bearer, wrong body token)
   let bad ← Grpc.Channel.unary chRR serviceName "Stamp"
     (StampRequest.encode { token := "nope", billet := "x" })
   checks := checks.push (
@@ -121,7 +144,7 @@ def main (args : List String) : IO UInt32 := do
   -- Act VIII: Binary log
   let sink ← Grpc.BinaryLog.newSink
   let logged ← Grpc.BinaryLog.logUnaryCall sink 7 chRR serviceName "Stamp"
-    (StampRequest.encode { token := accessToken, billet := "logged" })
+    (StampRequest.encode { token := accessToken, billet := "logged" }) stampAuthMd
   checks := checks.push (expectOk "act.binlog.call" logged.status.code)
   let ev ← Grpc.BinaryLog.events sink
   checks := checks.push (
@@ -149,7 +172,7 @@ def main (args : List String) : IO UInt32 := do
   -- Act XI: SlowStamp (plain unary; hedging races use background tasks that can
   -- keep the process alive, so we only assert the config parse + a slow RPC OK).
   let slow ← Grpc.Channel.unary chRetry serviceName "SlowStamp"
-    (StampRequest.encode { token := accessToken, billet := "anneal" })
+    (StampRequest.encode { token := accessToken, billet := "anneal" }) stampAuthMd
   checks := checks.push (expectOk "act.slow_stamp" slow.status.code)
 
   let mut failed : Nat := 0

Examples/MirrorForge/README.md

@@ -8,9 +8,9 @@ Two forge processes (`alpha` / `beta`) sit behind a round-robin channel. The cli
 
 | Act | What it exercises |
 |---|---|
-| Stamp ×2 + interceptor | Unary + client logging interceptor + forge mark |
+| Stamp ×2 + interceptor | Unary + client logging interceptor + forge mark; **Bearer metadata** (body token fallback) via `registerUnaryWithContext` |
 | Round-robin | `LEAN_GRPC_RESOLVE_ADDRS` + `loadBalancingPolicy=round_robin` → different `forgeId`s |
-| Auth reject | Body token gate → `UNAUTHENTICATED` |
+| Auth reject | Missing/wrong credentials → `UNAUTHENTICATED` |
 | Quench + retry | First `UNAVAILABLE`, client `retryPolicy` recovers |
 | Health Check/Watch | Standard health service |
 | Reflection v1alpha + v1 | `list_services` includes forge + health |
@@ -27,3 +27,20 @@ Two forge processes (`alpha` / `beta`) sit behind a round-robin channel. The cli
 ```
 
 Exit `0` = all checks passed.
+
+## Optional TLS / mTLS
+
+Default listen is h2c. To exercise 1.1.0 peer identity:
+
+```bash
+# Server (each forge):
+TLS_CERT=certs/server.crt TLS_KEY=certs/server.key TLS_CLIENT_CA=certs/ca.crt \
+  FORGE_ID=alpha GRPC_PORT=50201 ./.lake/build/bin/mirrorForgeServer
+
+# Client:
+TLS_CA=certs/ca.crt TLS_CERT=certs/client.crt TLS_KEY=certs/client.key \
+  TLS_SERVER_NAME=127.0.0.1 \
+  ./.lake/build/bin/mirrorForgeClient 127.0.0.1 50201 50202
+```
+
+With `TLS_CLIENT_CA` set, Stamp runs `requirePeerIdentity` and embeds the peer CN in the stamp mark (`{forgeId}:{cn}:{billet}`).

Examples/MirrorForge/Server.lean

@@ -7,7 +7,22 @@ import Examples.MirrorForge.Protocol
 
 open Examples.MirrorForge.Protocol
 
-/-- One forge mirror. Set `FORGE_ID` / `GRPC_PORT` (defaults: alpha / 50201). -/
+/-- Accept forge credentials from Bearer metadata **or** body `token` (fallback for
+    existing h2c MirrorForge clients). Under mTLS, `requirePeerIdentity` may also
+    sit on the interceptor chain. -/
+private def authorized (ctx : Grpc.ServerCallContext) (bodyToken : String) : Bool :=
+  match ctx.metadata.get? "authorization" with
+  | some auth =>
+      auth == s!"Bearer {accessToken}" || bodyToken == accessToken
+  | none =>
+      bodyToken == accessToken
+
+/-- One forge mirror. Set `FORGE_ID` / `GRPC_PORT` (defaults: alpha / 50201).
+
+    TLS (optional):
+    * `TLS_CERT` / `TLS_KEY` — serve with in-process TLS+ALPN `h2`
+    * `TLS_CLIENT_CA` — require and verify client certs (mTLS); Stamp uses
+      `requirePeerIdentity` and embeds peer CN in the stamp mark when present -/
 def main : IO Unit := do
   let port := ((← IO.getEnv "GRPC_PORT").getD "50201").toNat?.getD 50201 |>.toUInt16
   let forgeId := (← IO.getEnv "FORGE_ID").getD "alpha"
@@ -22,25 +37,39 @@ def main : IO Unit := do
   let flakyLeft ← IO.mkRef (1 : Nat)  -- first Quench fails with UNAVAILABLE
   let logSink ← IO.mkRef (#[] : Array String)
 
-  let chain : Array Grpc.Interceptor.ServerUnary := #[
-    Grpc.Interceptor.loggingServer logSink
-  ]
+  let cert := (← IO.getEnv "TLS_CERT").getD ""
+  let key := (← IO.getEnv "TLS_KEY").getD ""
+  let clientCa ← IO.getEnv "TLS_CLIENT_CA"
+  let useTls := !cert.isEmpty && !key.isEmpty
+  let mtls := useTls && clientCa.isSome
+
+  let mut chain : Array Grpc.Interceptor.ServerUnaryWithContext :=
+    #[Grpc.Interceptor.loggingServerWithContext logSink]
+  if mtls then
+    chain := chain.push Grpc.Interceptor.requirePeerIdentity
 
   let mut s := Grpc.Server.empty
 
-  -- Stamp: token-gated unary through interceptor chain
-  s := Grpc.Interceptor.registerUnary s serviceName "Stamp" chain fun reqBytes => do
+  -- Stamp: context-aware unary (Bearer metadata preferred; body token fallback)
+  s := Grpc.Interceptor.registerUnaryWithContext s serviceName "Stamp" chain fun ctx reqBytes => do
     let req ← IO.ofExcept (StampRequest.decode reqBytes)
-    if req.token != accessToken then
+    if !(authorized ctx req.token) then
       Grpc.Channelz.recordFailure counters
       return (ByteArray.empty, Grpc.Status.unauthenticated "bad forge token")
     if req.billet.isEmpty then
       Grpc.Channelz.recordFailure counters
       return (ByteArray.empty, Grpc.Status.invalidArgument "empty billet")
     let report ← orcaRef.get
+    let peerCn :=
+      match ctx.peerIdentity with
+      | some id => id.commonName
+      | none => ""
+    let mark :=
+      if peerCn.isEmpty then s!"{forgeId}:{req.billet}"
+      else s!"{forgeId}:{peerCn}:{req.billet}"
     let reply := StampReply.encode {
       forgeId
-      mark := s!"{forgeId}:{req.billet}"
+      mark
       cpuLoad := report.cpuUtilization
     }
     Grpc.Channelz.recordSuccess counters
@@ -79,5 +108,15 @@ def main : IO Unit := do
     s := Grpc.Channelz.register s counters
   | _ => pure ()
 
-  IO.println s!"MirrorForge[{forgeId}] on 127.0.0.1:{port.toNat}"
-  Grpc.Server.serveH2c s { host := "127.0.0.1", port }
+  if useTls then
+    let tlsCfg : Grpc.Tls.Config := {
+      certPath := some (System.FilePath.mk cert)
+      keyPath := some (System.FilePath.mk key)
+      clientCaPath := clientCa.map System.FilePath.mk
+    }
+    let mtlsNote := if mtls then " (mTLS)" else ""
+    IO.println s!"MirrorForge[{forgeId}] TLS+ALPN on 127.0.0.1:{port.toNat}{mtlsNote}"
+    Grpc.Server.serveTls s tlsCfg { host := "127.0.0.1", port }
+  else
+    IO.println s!"MirrorForge[{forgeId}] on 127.0.0.1:{port.toNat}"
+    Grpc.Server.serveH2c s { host := "127.0.0.1", port }

Grpc.lean

@@ -11,6 +11,7 @@ import Grpc.StatusDetails
 import Grpc.Compression
 import Grpc.Message
 import Grpc.Metadata
+import Grpc.PeerIdentity
 import Grpc.Server
 import Grpc.Client
 import Grpc.Stream
@@ -38,5 +39,5 @@ import Grpc.Grpclb
 import Grpc.Interceptor
 
 namespace Grpc
-def version : String := "1.0.0"
+def version : String := "1.1.0"
 end Grpc

Grpc/Codegen/Emit.lean

@@ -450,6 +450,11 @@ def emitServiceTyped (pkg : String) (svc : ServiceDescriptor) : Except String St
         out := out ++ "    | .ok req =>\n"
         out := out ++ "      let (resp, st) ← h req\n"
         out := out ++ s!"      return ({respTy}.encode resp, st)\n\n"
+        out := out ++ s!"/-- Register a typed unary handler with `ServerCallContext` for `{svc.name}/{m.name}`. -/\n"
+        out := out ++ s!"def register{svc.name}{m.name}WithContext (s : Grpc.Server)\n"
+        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"
     return out
 
 /-- Emit one `.lean` file's worth of message structs + typed client/server code for a single

Grpc/Interceptor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import Grpc.Server
 import Grpc.Channel
+import Grpc.PeerIdentity
 
 /-! # Client/server interceptor chains for unary calls.
 
@@ -27,6 +28,27 @@ def registerUnary (s : Server) (service method : String) (chain : Array ServerUn
     (h : UnaryHandler) : Server :=
   Server.register s service method (applyServer service method chain h)
 
+/-- Context-aware server unary interceptor. -/
+abbrev ServerUnaryWithContext :=
+  String → String → UnaryHandlerWithContext → UnaryHandlerWithContext
+
+/-- Fold a chain of context-aware server interceptors around `base`, outermost-first. -/
+def applyServerWithContext (service method : String) (chain : Array ServerUnaryWithContext)
+    (base : UnaryHandlerWithContext) : UnaryHandlerWithContext :=
+  chain.foldr (fun mw next => mw service method next) base
+
+/-- Register a context-aware unary method wrapped with `chain`. -/
+def registerUnaryWithContext (s : Server) (service method : String)
+    (chain : Array ServerUnaryWithContext) (h : UnaryHandlerWithContext) : Server :=
+  Server.registerWithContext s service method (applyServerWithContext service method chain h)
+
+/-- Fail closed under mTLS: when `ctx.mtlsRequired` and `peerIdentity` is missing, return
+    `UNAUTHENTICATED` instead of invoking `next`. -/
+def requirePeerIdentity : ServerUnaryWithContext := fun _service _method next ctx req => do
+  if ctx.mtlsRequired && ctx.peerIdentity.isNone then
+    return (ByteArray.empty, Status.unauthenticated "mtls_required")
+  next ctx req
+
 /-- Client-side unary invoker: request bytes → `CallResult` (matches `Channel.unary`'s core
     shape, modulo the extra dialing options `Channel.unary` takes). -/
 abbrev ClientUnaryInvoker := ByteArray → IO CallResult
@@ -54,6 +76,18 @@ def loggingServer (sink : IO.Ref (Array String)) : ServerUnary := fun service me
   sink.modify (·.push s!"< {service}/{method} resp={resp.size}B status={st.code.toUInt32}")
   return (resp, st)
 
+/-- Context-aware variant of `loggingServer` (logs peer CN when present). -/
+def loggingServerWithContext (sink : IO.Ref (Array String)) : ServerUnaryWithContext :=
+  fun service method next ctx req => do
+    let peer :=
+      match ctx.peerIdentity with
+      | some id => id.commonName
+      | none => "-"
+    sink.modify (·.push s!"> {service}/{method} req={req.size}B peer={peer}")
+    let (resp, st) ← next ctx req
+    sink.modify (·.push s!"< {service}/{method} resp={resp.size}B status={st.code.toUInt32}")
+    return (resp, st)
+
 /-- Ready-made client interceptor: same as `loggingServer`, mirrored for the call site. -/
 def loggingClient (sink : IO.Ref (Array String)) : ClientUnary := fun service method next req => do
   sink.modify (·.push s!"> {service}/{method} req={req.size}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.0.0") : Hpack.HeaderField :=
+def userAgent (version : String := "1.1.0") : Hpack.HeaderField :=
   ⟨ascii "user-agent", ascii s!"grpc-lean/{version}"⟩
 
 def http415 : Array Hpack.HeaderField :=

Grpc/Native/Tls.lean

@@ -3,6 +3,7 @@ Copyright © 2026, Riley Betts Ltd (rileybetts.ai)
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import H2.Transport
+import Grpc.PeerIdentity
 
 namespace Grpc.Native.Tls
 
@@ -44,6 +45,11 @@ opaque recv (c : @& Conn) (maxBytes : @& Nat) : IO (Option ByteArray)
 @[extern "lean_grpc_tls_close"]
 opaque close (c : @& Conn) : IO Unit
 
+/-- Extract verified peer certificate identity after a TLS(/mTLS) handshake.
+    Returns `none` when the peer presented no certificate. -/
+@[extern "lean_grpc_tls_peer_identity"]
+opaque peerIdentity? (c : @& Conn) : IO (Option PeerIdentity)
+
 /-- ByteTransport over an in-process TLS connection. -/
 def transport (c : Conn) : H2.ByteTransport where
   send := fun b => send c b

Grpc/PeerIdentity.lean

@@ -0,0 +1,37 @@
+/-
+Copyright © 2026, Riley Betts Ltd (rileybetts.ai)
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Grpc.Metadata
+
+namespace Grpc
+
+/-- Verified TLS peer certificate identity.
+    Fields come **only** from the peer cert on the TLS connection (via OpenSSL),
+    never from client-supplied gRPC metadata.
+
+    `subjectDn` uses OpenSSL RFC 2253 one-line form (`XN_FLAG_RFC2253`). -/
+structure PeerIdentity where
+  subjectDn : String
+  commonName : String
+  dnsSans : Array String
+  uriSans : Array String
+  fingerprintSha256 : String
+  serial : String := ""
+  deriving Inhabited, Repr
+
+/-- Per-RPC server context for unary handlers registered with `registerWithContext`.
+
+    * `peerIdentity` — `some` after mTLS when a client cert was presented and verified;
+      `none` on h2c, TLS without client cert, or when no peer cert is available.
+    * `metadata` — inbound request headers (HTTP/2 lowercased names; excludes `:pseudo`).
+    * `methodPath` — e.g. `/svc/Method`.
+    * `mtlsRequired` — `true` when the listener was configured with `clientCaPath`. -/
+structure ServerCallContext where
+  peerIdentity : Option PeerIdentity := none
+  metadata : Metadata := {}
+  methodPath : String := ""
+  mtlsRequired : Bool := false
+  deriving Inhabited
+
+end Grpc