QUIC v1/v2 and HTTP/3 for Rust, using Hibana to express protocol order and transfer ownership between roles. TLS is provided by hibana-tls.
The library is no_std, forbids unsafe Rust, and does not link the alloc crate.
Connection entry points borrow their stream slots and runtime arenas from the caller.
TLS, routing and protocol futures use bounded storage. hibana-quic-pal supplies Linux/macOS UDP,
readiness, clocks, entropy and file access; it contains no protocol choreography.
This is experimental software; passing interoperability tests does not establish
complete cryptographic security.
The protocol order is executable: the same global choreography that explains who may act next is projected into the per-role programs enforced by the running endpoints. QUIC receive, TLS, transmit, UDP publication, timers and retirement are separate participants in that choreography.
- Declare the order. QUIC choreography()composes Retry, early data, receive/transmit, timers and Initial-key retirement withseq,par,routeandroll.
- Project and attach. localside::Endpoints::attachtakes that global directly, derives eachRoleProgramwithproject, and enters the session to obtain each affineEndpoint. It also installs the physical-send resolver. There is no separate connection-program bundle.
- Execute the localsides. The local composition
runs the actual receive,
transmit,
publication and
timer continuations. Their send,recvandofferoperations must follow the role projections. Handshake packet storage and decoding perform authentication and CRYPTO reassembly without advancing endpoints.
- Move resources with the protocol. Application admission moves the transmit continuation, authenticated Finished receipt and transcript through owned slots. It checks their connection scope before admitting application traffic. A message label alone is not a substitute for those resources.
A role identifier names a participant in the global. A projected RoleProgram
describes its permitted operations. An Endpoint is that participant's affine,
attached protocol capability. The actual computation is an async localside that
owns or exclusively borrows endpoints and resources. A role identifier is not a
thread, and an endpoint does not spawn or poll its localside.
For a complete connection, follow these concrete definitions:
- Application global: role identifiers, choreography and role projections, including the TLS/QUIC prefix.
- Application locals: Endpoints, the endpoint-to-consumer inventory, andEndpoints::attachin the same file.
- Application execution: construction of
each receive, source, sink, key, timer, publication and retirement future;
the TaskSetlisting those futures is the actual concurrent execution set.
- Caller-owned session: session storage, program projection, endpoint attachment and the call into that execution.
- Handshake locals and their execution: the same ownership/attachment and execution split for the authenticated prefix.
Some localsides hold several endpoints; for example, application receive holds
receive, rx_keys and peer_event. Startup and retirement also borrow these
endpoints in the order required by the global. Their fields document the
consumers rather than pretending there is one task for every endpoint.
runtime::TaskSet polls the composed local futures; it does
not choose QUIC/TLS protocol transitions. On native systems, the PAL
Reactor::block_on supplies polling and I/O wakeups.
The command-line examples use std for arguments and diagnostics; positional file access is supplied by PAL. Their application endpoints and connection storage follow the same allocator-free library API. With caller-owned storage, another executor can poll the same connection future.
For an application defined with its own global, session execution
attaches its projected endpoint and joins its application localside with the
network localside. The raw QUIC example passes
its projected program and an inferred async application localside directly into that entrypoint.
Application code starts with session, a shared application global and its
client/server localsides, as shown in the examples below. Endpoint projection
and application execution use the same types on native and caller-owned paths.
For a custom connection, quic::application::{Buffers, Setup} supplies storage
and parameters. Use quic::application::localside::Endpoints for attachment,
Buffers and Setup for caller-owned resources, and the corresponding localside
to run them. Caller-owned stream arrays and arenas are grouped by session::ConnectionMemory;
session::Memory additionally owns the application carrier arena.
Packet codecs (quic::packet), transport parameters (quic::transport_parameters),
recovery receipts (quic::recovery) and publication capabilities
(quic::publication) are the low-level public interfaces used by diagnostic tools.
Their definitions remain with the implementation components under imp/; the
imp module itself is private. Public exports name the actual types and functions,
without a second wrapper or an alternate protocol owner.
Each protocol group has a global for permitted communication, a localside/ for
actual endpoint-owning execution, and imp for byte storage and computation.
An embedded group reuses endpoints from the containing connection; it does not
create a duplicate session or a second controller.
- QUIC handshake and connected application: their localside/mod.rsdefines and attaches the endpoint set;localside/run.rsassembles the actual futures.
- Retry admission: global →
server locals. receiveattaches INPUT, OWNER and OUTPUT and joins incoming, admission and outgoing operations.
- ECN: global → owner local. Its owner and the publication local share the complete connection projection.
- Path validation: global → owner local; address and probe observations are separate implementation data.
- Early data: global → quarantine owner, composed with the connected early locals.
- HTTP/3 control: global → actual control owner. The connection's source and sink share that choreography. Codecs and retained bytes do not select the next endpoint operation.
- HTTP/3 message exchange: global → reader/writer locals → attachment and join.
- User application: shared example global → client or server → session attachment. The HTTP/3 example uses the same application-level structure.
The scheduler and PAL supply polling, wakeups and physical I/O. The above globals and endpoint operations enforce protocol progress. The concrete checks and their limits follow below.
At each attached endpoint, Hibana checks the permitted operation, peer, direction, lane, label and schema before committing progress. A successful operation advances once; rejected or uncommitted operations do not grant a second transition. Affine endpoint ownership prevents cloning an endpoint to publish the same progress twice. These are runtime protocol checks combined with Rust ownership, not a claim that every invalid program fails to compile.
Rust moves and scoped borrows separately enforce resource ownership. For example, stream reclamation joins source, input and delivery receipts for the same identity before releasing storage; key ownership separates receive-side control from transmit-side sealing authority.
Hibana does not prove the QUIC algorithms, certificate validation, cryptographic arithmetic, constant-time execution or network reliability. Progress also depends on a live carrier and fair scheduling. Cancellation must settle or quarantine accepted native I/O. A submitted datagram is not evidence of peer delivery.
- Lean: abstract invariants for body ownership and EOF, stream-slot binding, cancellation and reclamation.
- Z3: counterexample searches over the corresponding constraints, including body completion and resource identity and drain conditions. Unsatisfiability establishes the encoded property under its model assumptions.
- Miri: the TLS secret-memory boundary tests execute under Rust's interpreter
to check the exercised unsafe memory operations and aliasing obligations. The
source and tests live in hibana-tls/src/secret.rsandsrc/secret/memory.rs.
- Rust and interoperability tests: actual endpoint execution, cancellation, loss/corruption and transfer tests connect those models to concrete behavior; Neqo/quiche peers check wire interoperability.
The Lean/Z3 models are not an extraction or end-to-end proof of the Rust code. Miri checks the executions it runs; it does not prove cryptographic strength or constant-time machine code. See Hibana's guarantee boundary for the underlying runtime and carrier assumptions.
The examples keep native initialization in one environment module.
It selects credentials, capacities and addresses. PAL supplies file access,
UDP, clocks, entropy and the executor. The CLI uses std for arguments and
output; the protocol library and PAL require neither std nor alloc.
Client and server project the same application conversation. The ordered QUIC
stream carries its typed messages using ALPN hibana/1. The application writes
send and recv; it never implements a carrier or drives transport phases.
//! One application choreography projected by both client and server.
//! Each launcher projects its role and supplies an inferred application localside.
use hibana::g;
use hibana::runtime::program::Projectable;
pub const CLIENT: u8 = 0;
pub const SERVER: u8 = 1;
pub type Number = g::Msg<0, u64>;
pub type Square = g::Msg<1, u64>;
pub fn choreography() -> impl Projectable {
g::seq(
g::seq(
g::send::<CLIENT, SERVER, Number>(),
g::send::<SERVER, CLIENT, Square>(),
),
g::seq(
g::send::<CLIENT, SERVER, Number>(),
g::send::<SERVER, CLIENT, Square>(),
),
)
}Complete executable. The endpoint argument is inferred.
//! Application global and localside; native initialization is in ../environment.rs.
#[path = "../environment.rs"]
mod environment;
mod global;
use global::{Number, Square};
use hibana::runtime::program::project;
use hibana_quic::session::Protocol;
fn main() -> Result<(), String> {
environment::client(Protocol::default(), async |client| {
client
.run(
project::<{ global::CLIENT }>(&global::choreography()),
async |client| -> Result<(), ApplicationError> {
for number in [42_u64, 7] {
client
.send::<Number>(&number)
.await
.map_err(ApplicationError::Protocol)?;
let square = client
.recv::<Square>()
.await
.map_err(ApplicationError::Protocol)?;
if square != number * number {
return Err(ApplicationError::IncorrectSquare);
}
}
Ok(())
},
)
.await
})?;
println!("42 squared = 1764\n7 squared = 49");
Ok(())
}
#[derive(Debug)]
pub enum ApplicationError {
Protocol(hibana::EndpointError),
IncorrectSquare,
}Complete executable. The endpoint argument is inferred.
//! Application global and localside; native initialization is in ../environment.rs.
#[path = "../environment.rs"]
mod environment;
mod global;
use global::{Number, Square};
use hibana::runtime::program::project;
use hibana_quic::session::Protocol;
fn main() -> Result<(), String> {
environment::server(Protocol::default(), async |server| {
server
.run(
project::<{ global::SERVER }>(&global::choreography()),
async |server| -> Result<(), ApplicationError> {
for _ in 0..2 {
let number = server
.recv::<Number>()
.await
.map_err(ApplicationError::Protocol)?;
let square = number
.checked_mul(number)
.ok_or(ApplicationError::Overflow)?;
server
.send::<Square>(&square)
.await
.map_err(ApplicationError::Protocol)?;
}
Ok(())
},
)
.await
})?;
println!("served two requests");
Ok(())
}
#[derive(Debug)]
pub enum ApplicationError {
Protocol(hibana::EndpointError),
Overflow,
}The application defines its g choreography and executes real Hibana
Endpoint::send, recv, and offer operations. The HTTP codecs implement
ordinary HEADERS, DATA, trailers and stream FIN. No application-message envelope
is added to the HTTP/3 wire.
The server application composes:
pub fn choreography() -> impl Projectable {
g::seq(
g::send::<READ, WRITE, RequestMethod>(),
g::par(request::<READ, APP>(), response::<APP, WRITE>()),
)
}Its localside receives actual HTTP fields and selects GET/HEAD /hello, streaming
POST /echo, or 404. For example, header publication is explicit:
app.recv::<Headers>().await?;
let fields = request.fields()?;
let metadata = fields.section().metadata;
// Inspect method/path and select the application's response.
drop(fields);
app.send::<Stored>(&()).await?;
response.response(200, &[(b"content-type", b"text/plain")])?;
app.send::<Headers>(&()).await?;
app.recv::<Stored>().await?;Every operation on Exchange is synchronous storage access only. fields() and
body(length) return owned slice loans; dropping a loan returns that actual
resource, but does not send a message. write(bytes) copies one bounded chunk
into the existing output slot and returns the length to send as Data. The
application explicitly drops each incoming loan before sending Stored, and
waits for outgoing Stored before reusing output storage. Attempting to reuse storage while its loan is outstanding fails the exchange; Hibana orders the messages, while Rust and
storage ownership protect the bytes. A receipt is not a peer acknowledgment.
The client application likewise defines its global and independent upload/download localsides, including informational headers and trailers. Its actual writer-derived request method goes directly to the response reader and then to the application. The application cannot replace the reader's HEAD/CONNECT semantics. Native readers and writers validate content lengths, bodyless responses, trailers and peer field-section limits.
Client and server globals coordinate their own local participants. They are not
presented as projections of one shared distributed application global. The
.http3 convenience binding admits exactly its documented client or server
roles. Additional application roles require an explicit rendezvous owner using
the public reader/writer codec localsides. The test suite demonstrates a result
role after the HTTP fragment. Merely passing an arbitrary graph does not make
this fixed binding execute its other roles. Compositions must preserve each
codec's fragment and Hibana's causal handoff requirements; serializing arbitrary
fragments is not automatically valid.
These bindings run one exchange on stream zero. Storage bounds in-flight chunks, not total body size. The local carrier still carries only unit/length control messages, so the direct API adds no body-payload copies. It does not claim end-to-end zero-copy. All streaming output remains provisional until message and connection completion. Errors or cancellation retire every role of the exchange; never resume a partially cancelled exchange.
The native client and server launchers contain only environment and binding setup; credentials, sockets, clocks and entropy remain in the shared environment module.
The native launchers target Linux/macOS with Rust 1.95. Supply a development
certificate chain/key for DNS:localhost and its CA. Verification stays enabled.
cargo build --locked --release --manifest-path examples/Cargo.toml --examples
# In separate terminals:
examples/target/release/examples/quic-server 127.0.0.1:4433 chain.pem key.pem
examples/target/release/examples/quic-client 127.0.0.1:4433 ca.pem
# Or run the HTTP/3 pair:
examples/target/release/examples/http3-server 127.0.0.1:4433 chain.pem key.pem
examples/target/release/examples/http3-client 127.0.0.1:4433 ca.pemUse the actual target directory when setting CARGO_TARGET_DIR. The raw example
calculates two squares; HTTP/3 defaults to a streaming POST to /echo. Set
HTTP_METHOD=GET or HEAD for /hello; HTTP_PATH=/missing demonstrates 404.
HTTP_BODY sets the POST body, which is streamed through bounded storage.
Both bindings require normal connection termination, separately from local
message completion. A 30-second launcher deadline bounds each demonstration.
python3 tests/check_examples.py examples/target/release/examples chain.pem key.pem ca.pemAn endpoint send publishes to bounded carrier storage; it is not a remote ACK. A message storage receipt permits that borrowed buffer to be reused. Actual stream FIN, authenticated connection close and resource retirement remain QUIC obligations. Cancellation drops the joined futures and their owned resources; it never fabricates a missing application reply or successful stream EOF.
Network peers remain untrusted. Hibana checks local projected operations; TLS, HTTP field validation and QUIC's receive rules check their respective inputs. Raw typed messages preserve the session, source, destination, lane and label, with up to 256 payload bytes per frame and four queued frames. HTTP/3 carries standard HTTP/3 frames without that raw application-message envelope.
- Raw session attachment
- Native HTTP/3 server roles
- Native HTTP/3 client roles
- HTTP message order
- Borrowed request actions
- Response production
- Shared HTTP storage and QUIC byte grants
- Core platform contracts
- PAL native executor
Every protocol directory puts ordering first, execution second, and computation
below imp/:
Server Retry admission uses the same core global with the Retry input/owner/output localsides.
localside/mod.rs contains the composition or direct role entry. The role files
contain the actual endpoint operations; imp/ contains buffers, codecs and
arithmetic.
Enable hq explicitly to use HTTP/0.9 GET interoperability. It is disabled by
default in both QUIC and TLS. Enabling it keeps the libraries no_std and does
not link alloc. The profile borrows request paths, parses targets in-place,
and transfers caller-provided response storage through the existing connection
and stream choreography.
hq::Requests, hq::Response and hq::Service provide bounded
wire/storage effects. session::Client::transfer and session::Server::serve
own connection execution. Response accepts one response on stream 0;
multi-request clients provide their own StreamSink for per-stream storage.
Path authorization and percent-decoding policies belong to the application.
The HQ client and server
show a one-file exchange. Their Unix launchers use std for CLI/file setup;
the board entry points use the same operations
without std or alloc. The larger tests/interop/driver binary is the interoperability
runner adapter, with filesystem and test-scenario handling.
cargo test --locked --features hq
cargo check --locked --lib --features hq --target thumbv6m-none-eabi
cargo build --locked --release --manifest-path examples/Cargo.toml --features hq --example hq-client --example hq-servercargo check --locked --lib
cargo test --locked
cargo check --locked --lib --target thumbv6m-none-eabiFor development tests that use the sibling TLS sources, place hibana-tls/
next to hibana-quic/ at the revision pinned in Cargo.toml.
Licensed under MIT OR Apache-2.0; see LICENSE-MIT and LICENSE-APACHE.
The protocol implementation has one home in src/:
- QUIC global and localsides own the handshake and its affine continuations.
- Connected global and localsides own streams, keys, close and retirement.
- Retry global, server localsides and packet arithmetic perform admission with injected I/O.
- HTTP/3 message global, localsides and bounded codec consume message storage without filesystem assumptions.
- Application session connects user-projected localsides to the common stream implementation.
Borrowed connection attachment consumes
caller-owned slabs, buffers, keys and physical capabilities without allocating.
Connection attachment borrows the
caller-owned stream array and arena and calls that same attachment. There is no
alloc feature or allocator-backed alternative. Both OS and bare-metal callers
supply the same physical capabilities and poll the same Rust futures.
The environment supplies DatagramRx, DatagramTx, DatagramSocket and Clock, cryptographic Entropy, and an executor that polls ordinary Rust futures. Native implementations and minimal environment examples are under pal/.
For a board or custom OS, the Pico integration example
reuses the exact native example's application global and client/server localsides.
It accepts board I/O, credentials and caller-owned connection memory. It builds
without std or alloc; it is not a boot image, network driver, or evidence that
a particular board has enough RAM for a chosen connection profile.
cargo check --locked --manifest-path pal/examples/pico/Cargo.toml --target thumbv6m-none-eabi