HIBANA
hibana is a Rust 2024, #![no_std], no-alloc-oriented runtime for
affine multiparty session types.
It lets a protocol crate describe communication once as a global choreography,
project each participant into a compact local program, attach transport and
storage, and hand application code a small affine Endpoint.
The complete path is:
hibana::g choreography
-> integration::program::project(&program)
-> integration::SessionKit::enter(...)
-> Endpoint
-> flow().send() / recv() / offer() / RouteBranch::decode()
There are only two public surfaces:
| Surface | Used by | Main names |
|---|---|---|
| Application surface | application code | hibana::g, Endpoint, RouteBranch, EndpointResult, EndpointError |
| Integration surface | protocol and integration crates | hibana::integration, hibana::integration::program |
If you are writing an application, stay on hibana::g and Endpoint. If you
are implementing a protocol crate, use hibana::integration to project, attach,
bind transport, install policy, and return endpoints.
Install
Add Hibana from crates.io:
Or write the dependency explicitly:
[]
= "0.6.2"
The default feature set is empty. Hibana is #![no_std] and no-alloc-oriented
by default.
Enable std only for host-side tests, diagnostics, and documentation builds:
[]
= { = "0.6.2", = ["std"] }
What Hibana Is
Hibana is for communication systems where the protocol shape should be known before runtime.
You write one global choreography:
use g;
let app = seq;
The choreography says:
- role
0sends message label1with au32payload to role1on lane0; - role
1then sends message label2with au32payload back to role0.
A protocol crate composes any required prefixes, projects the choreography for
each role, attaches transport and storage, and returns an Endpoint. The
application then drives only its local endpoint.
Affine Ownership, Not Shared Protocol State
Hibana's semantics are affine endpoint ownership and endpoint progress. The
current protocol state is the projected continuation owned by an Endpoint;
it is not a shared flag, shared table, shared memory cell, or ambient runtime
variable.
Each role must advance through its endpoint. The only evidence that may affect protocol progress is evidence admitted by the projected descriptor through the attached transport, or an explicit resolver decision at a projected route / loop policy point. Role code must not read shared memory, shared atomics, global flags, device registers, or side-channel state to decide whether a route is ready, a loop continues, or a message may be skipped.
Shared memory is especially not protocol authority. An integration crate may
use memory, atomics, interrupts, DMA, or OS primitives as private transport or
resolver implementation mechanics, but those mechanics must first become
transport frames, descriptor-checked binding evidence, or resolver inputs at
explicit policy points. They never replace flow().send(), recv(),
offer(), or RouteBranch::decode().
Quick Start
Application code usually sees an endpoint that a protocol crate has already attached.
use g;
endpoint.?.send.await?;
let reply = endpoint..await?;
That is the main user path:
- define messages and choreography with
hibana::g; - receive an attached
Endpointfrom your protocol crate; - call
flow().send(),recv(),offer(), andRouteBranch::decode().
flow() and offer() are previews. Endpoint progress happens when a send or
decode succeeds. A failed preview does not move the endpoint and does not choose
an alternate route. Preview evidence can wake or guide polling, but it cannot
mint a continuation.
Application Guide
Application authors only need these names:
hibana::g::{Role, Msg, Program, send, seq, route, par}EndpointRouteBranchEndpointResult<T>EndpointError
The normal choreography language is:
use g;
let request = ;
let response = ;
let program = seq;
Keep choreography terms local. Compose them once and let the protocol crate
project them immediately. Program<S> is the typed choreography witness; it is
not a transport handle, heap object, or reusable runtime object.
Sending And Receiving
Use flow().send() when the next local step is a send known from the
choreography:
endpoint
.?
.send
.await?;
Use recv() when the next local step is a deterministic receive:
let value = endpoint..await?;
The message type carries the choreography label, payload type, and optional control kind. The runtime checks the projected descriptor and fails closed if the label, lane, payload shape, or control/data kind does not match.
Routes
g::route(left, right) is binary. Branch labels must be unique within the
route shape.
use g;
let accepted = ;
let rejected = ;
let routed = route;
When the endpoint reaches a route decision, call offer():
let branch = endpoint.offer.await?;
match branch.label
If the chosen route arm begins with a send, drop the preview branch and send the first message in that arm:
let branch = endpoint.offer.await?;
match branch.label
The route is never selected by parsing payload bytes. Route authority comes from the projected descriptor or from an explicit resolver decision at a projected route point. Transport observation may only supply demux evidence that is checked against descriptor metadata; a frame label, payload shape, or binding hint is never an independent route decision.
Failure, Deadlines, And Cancellation
Endpoint operations return EndpointResult<T>, so application code should use
ordinary ?:
endpoint.?.send.await?;
let reply = endpoint..await?;
let branch = endpoint.offer.await?;
let payload = branch..await?;
This shape has only two committed outcomes:
Ok(progress) next choreography state exists
Err(domain evidence) current session generation is terminal
Errors are not route arms. An operational deadline, transport close, decode failure, or protocol invariant failure poisons the affected session generation and returns diagnostic evidence. It does not authorize retry, reconnect, or a different branch in the same generation.
There is intentionally no recv_timeout, send_timeout, public cancel, or
same-generation recovery API. If time should select a branch, model time in the
choreography itself: use a timer or clock role and an explicit route point, then
install a resolver for that route. Runtime deadlines are integration fuses; they
kill the generation instead of becoming protocol-visible choices.
The public evidence envelopes are domain-specific:
EndpointErrorforflow,send,recv,offer, anddecode;ResolverErrorfor resolver registration and resolver decisions;AttachErrorfor rendezvous and endpoint attach.
There is no public wide HibanaError, and public error-kind enums are not part
of the application decision surface. The Debug output records the operation
and callsite so top-level runners and panic handlers can report where a failure
was observed without requiring wrapper errors at every call.
Parallel Composition
g::par(left, right) combines independent local flows. Empty arms and
overlapping (role, lane) ownership are rejected by projection.
use g;
let left = ;
let right = ;
let parallel = par;
Lanes are protocol-owned separation units. Application code should follow the
lane contract exposed by its protocol crate rather than assigning global lane
meaning inside hibana itself.
Payloads
Built-in exact codecs cover (), bool, integers, borrowed byte slices, and
fixed byte arrays. Fixed-width decoders reject trailing bytes.
Custom payloads implement hibana::integration::wire::WireEncode for sending
and hibana::integration::wire::WirePayload for receiving:
use ;
;
Decoded values may borrow from the received frame:
type BorrowedBytes = &'static ;
// In a message type, use `g::Msg<LABEL, &[u8]>`.
// The decoded value returned by recv/decode is borrowed from the transport frame.
Dynamic Policy
Dynamic policy is explicit. Mark the controller self-send that opens each
route or loop arm with Program::policy::<POLICY_ID>(), then let the
protocol crate install a resolver for that policy id. The policy annotation is
on the arm head, not on the g::route(...) wrapper.
use g;
use GenericCapToken;
use RouteDecisionKind;
const POLICY_ID: u16 = 7;
let left =
.;
let right =
.;
let routed = route;
Policy does not appear as driver if/else logic. It is a choreography point
resolved through the integration policy seam.
If a resolver returns Defer, the offer remains pending unless new route
evidence or a valid resolver decision appears. Hibana does not maintain
offer-time defer budgets, synthetic poll retries, or progress-exhaustion escape
paths.
An operational deadline may still kill the session generation, but that is a
terminal fault, not a protocol branch.
Control Messages
Control messages are ordinary choreography messages. A control message is
written as g::Msg<LABEL, GenericCapToken<K>, K>, where K implements the
protocol-neutral control-kind traits.
use g;
use GenericCapToken;
type Grant = Msg;
let control_step = ;
The message label is choreography identity. Control meaning comes from the control kind's descriptor metadata, not from reserved numeric labels.
There are two public layers:
GenericCapToken<K>plusControlResourceKindis the choreography message shape. It lets protocol crates write control steps as ordinaryg::send(...)nodes.integration::cap::advanced::ControlOpis the built-in descriptor opcode catalogue evaluated by the hibana control kernel.
Only route and loop decision owners are provided as built-in public kind types:
use g;
use GenericCapToken;
use ;
type Continue = Msg;
type Break = Msg;
let continue_step = ;
let break_step = ;
RouteDecisionKind, LoopContinueKind, and LoopBreakKind are local
self-send controls. They are how route arms and route-loop heads carry explicit
controller decisions without adding a second choreography language. They may be
used with Program::policy::<ID>() when a resolver must choose the arm.
The full built-in control-op catalogue is:
| Opcode | Meaning | Usual use |
|---|---|---|
ControlOp::RouteDecision |
Selects a binary route arm for a route scope. | RouteDecisionKind on the controller self-send, optionally resolver-backed. |
ControlOp::LoopContinue |
Selects the continue arm of a route loop. | LoopContinueKind at the loop head. |
ControlOp::LoopBreak |
Selects the break arm of a route loop. | LoopBreakKind at the loop head. |
ControlOp::Fence |
Orders or authorizes a protocol-visible control boundary without changing topology or transaction state. | Protocol-owned wire or local control barriers. |
ControlOp::StateSnapshot |
Records the current session/lane generation before a mutation. | Snapshot before transaction, abort, restore, or topology-sensitive mutation. |
ControlOp::StateRestore |
Restores previously snapshotted state after a failed or aborted mutation. | Rollback path paired with StateSnapshot. |
ControlOp::TxCommit |
Commits a snapshot-backed transaction and finalizes that lane generation. | At-most-once commit of a protocol mutation. |
ControlOp::TxAbort |
Aborts a snapshot-backed transaction and records the abort path. | Fail-closed transaction cancellation. |
ControlOp::AbortBegin |
Starts an explicit abort handshake. | First step of a protocol-owned abort sequence. |
ControlOp::AbortAck |
Acknowledges an abort handshake. | Idempotent acknowledgement for abort completion. |
ControlOp::TopologyBegin |
Opens a topology transition intent with source/destination rendezvous, lane, and generation facts. | Distributed lane/rendezvous reconfiguration. |
ControlOp::TopologyAck |
Validates and acknowledges a topology intent at the destination side. | Destination half of topology coordination. |
ControlOp::TopologyCommit |
Commits an acknowledged topology transition and bumps generation. | Source-side topology finalization. |
ControlOp::CapDelegate |
Delegates capability authority between control owners. | Lower-layer endpoint/rendezvous capability transfer. |
These opcodes are not new application commands. A protocol that needs topology,
transaction, abort, snapshot, fence, or delegation control still writes ordinary
choreography messages, usually with a protocol-owned ControlResourceKind that
maps to the relevant ControlOp. The runtime then consumes the projected
descriptor metadata fail-closed. Payload contents, labels, transport hints, and
driver if/else logic never become route or transaction authority.
ControlPath decides where the control is executed:
ControlPath::Localis a local self-send.g::sendrejects cross-role local controls.ControlPath::Wireis a wire-visible cross-role send.g::sendrejects self-sent wire controls.
A custom wire control kind separates message label and control metadata:
use ;
use ;
use ;
const CUSTOM_WIRE_MSG_LABEL: u8 = 200;
const CUSTOM_WIRE_TAP_ID: u16 = 0x03c8;
;
type CustomWireMsg =
Msg CUSTOM_WIRE_MSG_LABEL }, , CustomWireKind>;
Use AUTO_MINT_WIRE = true only when the endpoint can mint the wire token from
descriptor-backed policy inputs. Otherwise send an explicit
GenericCapToken<K> payload.
Topology and transaction control are integration-level tools, not application state machines. Use them when the protocol itself needs a choreography-visible state transition:
- topology: move or rebind a lane/rendezvous relation with
TopologyBegin -> TopologyAck -> TopologyCommit; - transaction: bracket a multi-step mutation with
StateSnapshot -> TxCommitorStateSnapshot -> TxAbort/StateRestore; - abort: make cancellation explicit with
AbortBegin -> AbortAck; - capability: delegate a control capability through
CapDelegatewhen the lower-layer endpoint token path owns that transfer; - fence: insert a protocol-owned ordering or readiness boundary without adding domain-specific APIs to hibana core.
Do not add g::topology, g::tx, driver-side retry loops, or payload-driven
branch selection. The authority source remains the choreography plus the
projected descriptor.
CapDelegate is special: generic app/protocol control kinds should not use it
as a plain custom message. Delegation requires the lower-layer endpoint token
path so the control kernel can canonicalize the transfer.
Protocol Integration
Protocol crates use the same hibana::g language as applications. There is
no second composition language.
Compose And Project
A protocol crate may place transport or appkit prefixes before the application choreography, then project each role.
use g;
use ;
let prefix = seq;
let app = seq;
let program = seq;
let client: = project;
let server: = project;
project(&program) is the projection boundary. Runtime code consumes the
projected descriptor; it does not rediscover protocol shape.
Attach An Endpoint
The canonical integration path is borrowed and caller-provided:
use integration;
use SessionId;
use ;
let mut tap_buf = ;
let mut slab = ;
let config = from_resources;
let clock = new;
let kit: SessionKit =
new;
let rv = kit.add_rendezvous_from_config?;
let endpoint = kit.enter?;
Config::from_resources takes only storage and clock. Lane domain, endpoint
lease capacity, and operational wait fuses are not caller-selected config. A
fresh rendezvous starts with no materialized lane storage and no endpoint lease
table. Role attach reads the projected resident descriptor, grows exactly the
lane tables and endpoint lease entries it needs, and preserves existing session
state if a later projected role needs a wider lane span. Operational fuses
belong to the transport/substrate owner and are reported by the transport
instance; expiry poisons the session generation and never selects a protocol
branch. Integration code must not pass caller-chosen lane windows, endpoint
counts, or deadline knobs.
Attach does not lower a projected role. Attach reads the pre-existing
CompiledRoleImage owned by the projected program image and initializes only
endpoint/session state. The role image already carries its CompiledProgramRef;
attach must not reconstruct that program ref from a transient role builder or
attach-time descriptor build path. The resident CompiledRoleImage is the
ROM/static descriptor input to attach, not a product of attach-time descriptor
construction. A role with no resident descriptor is not attachable.
The resident compiled image is the source of truth. Attach must not rebuild the
role descriptor or program descriptor through an alternate materialization path,
and must not reserve lowering scratch. Immutable queries against the resident
CompiledProgramImage are descriptor reads; they are not attach lowering and
must not allocate, clone, or reserve scratch. Runtime route-frontier workspace
is separate: it is descriptor-derived endpoint/session workspace for live
offer/decode state, not attach-time lowering scratch, and it must not overlap
payload scratch. If stable Rust cannot express a particular exact-sized static
layout, Hibana changes the resident image representation; it does not keep
attach-time lowering logic.
Runtime frontier entries are compact headers. They may remember live lane, scope, frontier, summary, and selection bits, but they must not cache descriptor-derived frame-label metadata, arm-materialization tables, route dispatch rows, or observed-state summaries. Those facts are read from the resident descriptor or recomputed from live evidence at the wait site. This keeps offer/frontier progress from reintroducing attach-time materialization through a different name.
The protocol crate owns concrete MyTransport and any binding state. The
application receives only Endpoint.
Useful integration owners:
integration::program::{project, RoleProgram, MessageSpec, StaticControlDesc}integration::SessionKitintegration::runtime::{Config, CounterClock, DefaultLabelUniverse, LabelUniverse}integration::ids::{EffIndex, Lane, RendezvousId, SessionId}integration::Transportintegration::binding::{BindingSlot, NoBinding}integration::policy::{ResolverContext, ResolverError, ResolverRef, RouteResolution, LoopResolution}integration::policy::signals::{PolicySlot, PolicySignals, PolicyAttrs, ContextId, ContextValue}integration::wire::{Payload, WireEncode, WirePayload}integration::cap::{GenericCapToken, ResourceKind, ControlResourceKind, CapShot, One, Many}integration::tap::TapEvent
Advanced buckets under integration::binding::advanced,
integration::transport::advanced, and integration::cap::advanced are for custom
integration code that needs demux metadata, transport observation, or
control-kind descriptor constants.
Transport
Implement integration::Transport to connect Hibana to an I/O system.
The transport owns:
open(local_role, session_id, lane)for role/session/lane-specific handles;poll_send(...)andpoll_recv(...);cancel_send(...)for transport cleanup when a send future is dropped;requeue(...)for frames that descriptor checks cannot consume yet;recv_frame_hint(...)as a non-blocking route-observation hint drain;drain_events(...),metrics(), andapply_pacing_update(...).
Transport sees bytes, frame labels, readiness, and metrics. It does not own
choreography meaning, route authority, retry policy, or cancellation semantics.
cancel_send(...) is not an application cancellation API; it is only a cleanup
hook for an uncommitted send preview.
The lane passed to open(...) is the logical lane owned by the returned
handles. A transport that multiplexes lanes over one carrier must preserve that
lane in carrier metadata and demultiplex before yielding payload bytes to the
endpoint. recv_frame_hint(...) must not consume payload bytes, but it is a
hint-drain: once it yields a frame label, it must not yield the same observation
again until poll_recv(...) or requeue(...) stages fresh receive state.
Route-observation hints are lane-scoped. A frame label alone is not route
authority; the endpoint checks any hint against projected lane and descriptor
metadata, and a hint can never select a route arm without resolver / route /
payload evidence.
Transport observation reaches resolvers as packed PolicyAttrs; custom
transports expose that view through
transport::advanced::TransportMetrics::attrs().
Binding
Use integration::binding::NoBinding when the transport can deliver the next
payload directly.
Use BindingSlot when the protocol has multiplexed streams or channels. A
binding slot may return IngressEvidence for a lane and later read from the
selected channel:
IngressEvidence is demux evidence only. It may support descriptor-checked
route observation, but it is not an independent route decision and must not be
used as dynamic route authority without resolver authority.
Resolver Policy
Resolvers are installed by the protocol crate for explicit policy points:
kit.?;
Policy inputs are slot-scoped. Resolver failure rejects the step; it does not fall through to a different semantic path.
Guarantees
Hibana keeps the public API small because the projection boundary carries the proof work.
Core guarantees:
- Rust 2024 and stable Rust
1.95; - default features are empty;
- runtime code is
no_stdand no-alloc-oriented; - descriptor storage is caller-provided, borrowed, static, or slab-backed;
- route shape, duplicate labels, malformed control paths, and lane ownership errors are rejected before endpoint execution;
- runtime cursor progress is one-way and affine;
- protocol state is affine endpoint ownership, not shared atomic or shared memory state;
- failed sends, receives, offers, and decodes do not authorize hidden progress;
- operational deadlines poison the current session generation and never select route arms;
- payload decode is exact;
- message logical labels and transport frame labels are separate concepts;
- control semantics are descriptor metadata, not reserved numeric labels;
- route authority is limited to projected facts and explicit resolver decisions; descriptor-checked transport observation may only confirm or demux projected facts.
What application code should not do:
- call transport APIs directly from localside logic;
- choose route arms by parsing payloads;
- model dynamic policy as driver-side branching;
- treat binding hints or frame labels as route authority;
- match endpoint errors to continue the same generation on a hidden alternate path;
- use shared memory, shared atomics, global flags, or side-channel state as route readiness, loop-control, or protocol-progress authority;
- expose protocol-specific APIs through the
hibanacrate root.
Validation
For a published crate consumer, the useful checks are ordinary Cargo commands:
For a repository checkout, maintainers should run the repository gate suite
before release. That suite protects the public surface, no_std build,
projection boundary, descriptor streaming, future layout, route authority, and
size measurements. It is intentionally kept outside the crate package.