http2-lean

HTTP/2 protocol foundations for Lean 4.

The project is in pre-release development. Version 0.1.0 is a development coordinate, not a compatibility promise, and public APIs may change before the first stable release.

Intended scope

The library provides application-independent HTTP/2 machinery:

• bounded incremental frame encoding and decoding;
• HPACK encoding, decoding, and dynamic-table management;
• settings, stream lifecycle, connection state, and error handling;
• connection- and stream-level flow control;
• header-block continuation and validation;
• Extended CONNECT support;
• transport-neutral state machines with explicit effectful adapters;
• managed h2c and TLS client connections for Extended CONNECT; and
• managed h2c and TLS listeners with graceful GOAWAY-based shutdown.

Application protocols and their message formats, metadata policies, status models, dispatch rules, and service runtimes are outside this library's scope. HTTP/1.1 remains a separate protocol concern.

Optional runtime-support targets provide callback-safe cancellation, bounded DNS lookup, canonical numeric destinations, socket-driven TLS sessions, system trust-anchor loading, and the narrow POSIX descriptor boundary required by trust loading. These adapters are not imported by the wire-protocol core.

The conformance targets are RFC 9113 for HTTP/2, RFC 7541 for HPACK, and the HTTP/2 protocol extension defined by RFC 8441. Server push is deliberately disabled; an endpoint advertises that policy and rejects an unexpected push promise as a connection protocol error.

Build

Bazel is the authoritative build and test system:

bazel build //...
bazel test //...

An optional Docker-backed interoperability smoke exercises the RFC 7541 HPACK boundary against a digest-pinned external tool. Its intentionally narrow scope and invocation are documented in Conformance/README.md.

The standalone dependency-mode check runs separately:

cd integration/downstream
bazel test //... --lockfile_mode=error

Lake supplies an editor project model and a compatibility build:

lake build

Library layers

The protocol core is exposed as @http2_lean//:http2_core. It contains no socket, TLS, DNS, or host-filesystem dependency. @http2_lean//:http2_client and @http2_lean//:http2_server add managed transports. The :http2 facade exports all three layers, while :runtime provides the optional environment adapters.

Client and server transports require the HTTP/2 connection preface and initial SETTINGS exchange. The cleartext entry points use prior-knowledge h2c; they do not implement an HTTP/1.1 Upgrade path. TLS entry points require ALPN h2. Connections retain their reader and writer owners until explicit close or server shutdown, and tunnel operations surface typed connection-, stream-, and local-input failures.

Bazel module

Consumers declare:

bazel_dep(
    name = "http2-lean",
    version = "0.1.0",
    repo_name = "http2_lean",
)
archive_override(
    module_name = "http2-lean",
    integrity = "sha256-rVteydmJ4HoqzdoL+9VEJMXCfJ07r++od1ftyBsnypI=",
    strip_prefix = "http2-lean-0.1.0",
    urls = [
        "https://github.com/pb64-lean/http2-lean/archive/refs/tags/v0.1.0.tar.gz",
    ],
)

The integrity value fixes the exact release contents even if a tag reference is changed upstream. Until all transitive modules are available through a Bazel registry, a root module must likewise provide immutable resolution for the dependencies declared in MODULE.bazel.

The public Lean import root is Http2. Optional application-independent adapters are imported through Http2.Runtime; their individual targets remain available when a consumer needs a smaller dependency closure.

Security

Bounded writers and native retirement

Client.Config.writerLimits, Server.Config.writerLimits, and the direct TLS session constructors accept positive byte/item limits (defaults: 8MiB/1024). Reservations include the send currently in flight, not only buffered FIFO entries. Producers never wait for capacity under a protocol/TLS mutex. Capacity exhaustion after protocol state has advanced poisons the connection; it never silently drops a frame or attempts an unsafe retry. TLS rejects an oversized application write before sealing and charges exact ciphertext bytes, including record overhead. Large application bodies should use acknowledged small chunks.

Failure/abort discards queued buffers and settles every acknowledged caller, including the in-flight ticket. Acknowledged success means the exact socket write completed, not merely that its bytes entered the queue. Graceful shutdown fences admission before draining. writerStats reports current/peak charges and rejections. After forced retirement, a charge can remain for an in-flight native send whose completion cannot be confirmed; it is not reported as reclaimed.

The pinned Std.Async.TCP/libuv API has no full cancel-send operation. The 200ms retirement windows bound Lean cleanup waits and cancel retained Lean tasks, but cannot promise that an already-issued native send has stopped or its buffer has been released. Socket shutdown is also bounded best effort. No hard real-time cancellation or complete native-ownership proof is claimed. Tests cover actual non-reading TCP peers, in-flight charging, byte/item overflow, close, injected writer failures, and exact ACK settlement.

Validate the pinned dependency graph with bazel test //... --lockfile_mode=error --jobs=4. For an editor/source check, use lake build. To work against local sibling sources, use lake --packages=lake-workspace.json build.

Remote peers and all received bytes are untrusted. Parsers and state machines must reject invalid input with typed failures, enforce configured bounds, and avoid silently weakening protocol requirements. The precise trusted boundary and supported-version policy are documented in SECURITY.md.

Please report suspected vulnerabilities privately rather than opening a public issue.

License

Licensed under the Apache License 2.0.