Source: docs/api-reference.md · Edit on GitHub

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.0.0).

Import umbrella: import Grpc (pulls status, channel, server, credentials, TLS, xDS, ops, etc.). Add import Proto for bundled message codecs.

The Lake lib Proofs is not part of the consumer API (CI-only compile-time theorems); see proofs.md.

Status and metadata

Grpc.Status / Grpc.StatusCode

gRPC status codes ok … unauthenticated. Helpers: Status.ok, .unimplemented, .internal, .deadlineExceeded, .cancelled, .unavailable, .invalidArgument, .permissionDenied, .resourceExhausted.

Optional detailsBin : Option ByteArray holds encoded google.rpc.Status when status ≠ OK.

Grpc.StatusDetails

  • encode / decode — google.rpc.Status via Proto.WellKnown.RpcStatus
  • attachBin — add grpc-status-details-bin
  • fromMetadata — read + reject contradicting codes / details on OK

Grpc.Metadata

API Purpose
add / get? ASCII metadata
addBin / getBin? -bin base64 (padded/unpadded)
percentEncode / percentDecode grpc-message
parseTimeoutMs 10S, 100m, 1H, 100u, 1n, …
statusHeaders / http200 / http415 / trailersOnly Response header builders
userAgent / schemeHttp / schemeHttps / methodPost / methodGet Pseudo/call-definition headers

Messages and compression

Grpc.Message

Length-prefixed gRPC frames (Compressed-Flag + 4-byte length + payload).

  • encode / decodeOne / decodeAll — pure (stored gzip for .gzip)
  • encodeIO / decode*IO — peer-compatible inflate/deflate via zlib helper / system gzip

Grpc.Compression.Algorithm

identity | gzip | deflate | snappy

  • negotiate — preference gzip > deflate > snappy > identity
  • compressIO / decompressIO — peer paths where available

Client

Grpc.CallResult

status, message (decoded payload bytes), headers, trailers.

Grpc.Client.unaryCall

Low-level unary on an H2.ClientConn (scheme http/https, user-agent, compression).

Grpc.Channel

API Purpose
connectH2c host port Plain h2c channel
dial target opts svc? Resolve + balanc + connect (dns:///, host:port, xds:///)
unary ch service method request metadata? timeout? compress? Unary RPC
openStream ch service method metadata? Interactive bidi client stream
serverStream / clientStream / bidiStream Batch streaming helpers (messages + status)
get / goAway / close Connection pool / drain
maxMsgSize / maxSendMsgSize / maxRecvMsgSize Message limits (default 4 MiB)
keepaliveMs Idle PING interval

Credentials.DialOptions: channel, call, authority.

Grpc.Stream

ClientStream with StreamWriter.send / sendAll / halfClose and StreamReader.recv? / recvAll / status. Server handler abbrevs: ServerStreamHandler, ClientStreamHandler, BidiStreamHandler.

Grpc.Interceptor

Unary middleware:

  • registerUnary / callUnary
  • applyServer / applyClient
  • Built-ins: loggingServer, loggingClient

Server

Grpc.Server

API Purpose
empty Empty registry
register Unary ByteArray → IO (ByteArray × Status)
registerServerStream / registerClientStream / registerBidi Streaming (raw bytes)
registerTyped / registerServerStreamTyped / registerClientStreamTyped / registerBidiTyped Streaming/unary with decode/encode adapters
serveH2c Listen h2c
serveTls Listen TLS+ALPN (via Tls.Config)
maxMsgSize Inbound limit

Bad content-type → HTTP 415. Unknown method / zero timeout → trailers-only gRPC status.

Ops registration

Module Register
Grpc.Health register / registerWithWatch (Check + streaming Watch)
Grpc.Reflection register (v1 + v1alpha list/file/symbol)
Grpc.Channelz register with IO.Ref Counters; recordSuccess / failures

Credentials and TLS

Grpc.Credentials

  • ChannelCredentials.insecure | .tls Tls.Config
  • CallCredentials.accessToken / .jwt / .oauth2 / .perRpc / .composite
  • DialOptions

Grpc.Tls.Config

certPath, keyPath, caPath, clientCaPath, serverName, alpn (default ["h2"]).

  • Client mTLS: set certPath + keyPath
  • Server mTLS: set clientCaPath on serve

Env: LEAN_GRPC_TLS_PROXY, LEAN_GRPC_TLS_INSECURE_FALLBACK=1 (dev only).

Grpc.Adc

  • accessToken / callCredentials / clearCache
  • dialOptions caPath? serverName? — TLS channel + ADC Bearer
  • Live check: scripts/run-adc-live.sh (manual)

Grpc.Gcp

Allowlisted: deferredCases = GCE channel credentials, ALTS. ADC call credentials are implemented.

Resolver, LB, retry, service config

Grpc.Resolver

parseTarget, resolve (multi-addr via getent ahosts; LEAN_GRPC_RESOLVE_ADDRS override).

Grpc.Balancer

Policy.pickFirst | .roundRobin; create, pick (RR advances per call).

Grpc.ServiceConfig

parse JSON for loadBalancingPolicy / loadBalancingConfig, timeout, retryPolicy, hedgingPolicy, methodConfig.

Grpc.Retry

shouldRetry, backoffMs from RetryPolicy.

Channel implements sequential retry and parallel hedging (RST losers).

Grpc.Grpclb

fetchServerList, decodeServerList, liveAddresses — thin BalanceLoad shim.

xDS

Grpc.Xds / Grpc.Xds.Discovery / Grpc.XdsAds

  • Type URLs for LDS / RDS / CDS / EDS / SDS
  • DiscoveryRequest/Response encode/decode; Request.ack / .nack
  • resolveChain — LDS→RDS→CDS→EDS
  • resolveFromEnv — LEAN_GRPC_XDS_BOOTSTRAP
  • CI: Tests/FakeAdsServer.lean, scripts/run-xds-ads-smoke.sh

Observability extras

Module Highlights
Grpc.Orca IEEE double utilization; per-RPC trailer + orca_oob
Grpc.BinaryLog Event sink for headers/messages/trailers
Grpc.Stats Counters; Prometheus text / OTel-stub exporter
Grpc.Jwt Unsigned JWT fixture helpers for interop

HTTP/2 (H2)

Consumers usually stay in Grpc.*. Useful lower APIs:

API Purpose
H2.Client.connectH2c / connectTransport Client connection
H2.Client.startRequest / awaitResponse / unary / resetStream Streams
H2.Client.rstToTrailers RST → synthetic gRPC trailers
H2.Server.listen / serveConn Server accept loop
H2.ByteTransport Pluggable send/recv
H2.handleFrame / ConnState State machine (tested via h2spec)

Protobuf (Proto)

Module Contents
Proto.Wire Varint, length-delimited, field decode helpers
Proto.WellKnown AnyMsg, map entries, RpcStatus (google.rpc.Status)
Proto.Message Interop messages (SimpleRequest, streaming, …)
Proto.RouteGuide RouteGuide example types

Codegen (Grpc.Codegen)

Executable protoc-gen-lean4-grpc:

  1. Text .proto (LEAN_GRPC_PROTO / argv) → Generated.lean with ByteArray RPC stubs
  2. protoc plugin — stdin CodeGeneratorRequest → stdout response with message structs + typed unary/streaming client stubs + typed unary server register helpers

Regenerate the helloworld example: scripts/gen-helloworld.sh (uses the same descriptor fixture as scripts/run-codegen-fixture.sh).

Current limits (descriptor path): nested messages, repeated, oneof, maps, and many scalar wire types are incomplete or fall back to bytes. Streaming server registration is not emitted — use Server.register*Typed. Stream client stubs are batch (send-all / recv-all), not interactive duplex.

Errors and mapping

Condition Application sees
Peer grpc-status Matching StatusCode
HTTP 415 invalidArgument (“unsupported media type”)
Other non-200 HTTP unknown (or existing grpc-status)
RST CANCEL cancelled
RST REFUSED_STREAM unavailable
RST ENHANCE_YOUR_CALM resourceExhausted
Client deadline deadlineExceeded (+ RST to peer)
Peer GOAWAY (new streams) unavailable
Oversized message resourceExhausted

Details: protocol-mapping.md.

Source: docs/api-reference.md in RileyBetts/lean-grpc. Hosted docs may lag the repository slightly.