Hibana lets Rust programs execute a finite multiparty protocol from one global choreography. The choreography is projected into a compact program for each role, and every send, receive, or route step must match that program before progress commits.
Hibana is a choreography-derived runtime enforcement kernel. It is
unconditionally no_std, needs no allocator, and uses caller-provided storage.
Protocol state is kept in compact descriptors instead of a distinct Rust
continuation type for every state, so protocol growth does not become endpoint
type growth.
- one choreography for up to 256 roles using the complete one-byte role domain;
- asynchronous send,seq,par, binaryroute, and guardedroll;
- affine endpoints that may be dropped but cannot publish progress twice;
- transport-neutral integration through one Transporttrait;
- the same public API on hosted and embedded targets.
Role IDs cover 0..=255. Projection, route participation, and attachment
accounting derive storage from actual events and local participants; the runtime
does not reserve a 256-entry role table. Splitting a protocol across several
sessions still changes the guarantee boundary: Hibana checks each session, not
the original choreography as one global protocol.
Hibana does not implement a network stack or a distributed algorithm. It enforces the protocol at each attached endpoint and states the carrier, deployment, codec, and scheduling conditions needed to lift that local result to a distributed guarantee.
This README is arranged by responsibility:
Add the crate:
cargo add hibanaThe crate uses Rust 2024 and requires stable Rust 1.95 or newer. It has no
normal dependencies and no feature-selected hosted variant.
Run the complete two-role example from a repository checkout:
cargo run --example ping_pongping=7, pong=8
The example is self-checking, ships in the published package, and is executed
by the release gate. Read the complete source in
examples/ping_pong.rs. Its protocol is small enough
to see in one place:
use hibana::{
g::{self, Msg},
runtime::program::{RoleProgram, project},
};
fn ping_pong() -> (RoleProgram<0>, RoleProgram<1>) {
let choreography = g::seq(
g::send::<0, 1, Msg<1, u32>>(),
g::send::<1, 0, Msg<2, u32>>(),
);
(project(&choreography), project(&choreography))
}The executable example adds caller-owned runtime storage and an in-memory host
transport, attaches both role programs to one SessionId, and drives the two
endpoints with send() and recv(). An embedded deployment supplies its own
transport, storage budget, and executor; the choreography and endpoint
operations stay the same.
global choreography
-> project(&choreography) once per role
-> compact RoleProgram descriptors
-> attach each role to one SessionId
-> drive Endpoint::send / recv / offer
-> commit exactly one permitted step or fail the session generation
Multiparty means peer, direction, and order come from one choreography projected for every role. Asynchronous means a successful send transfers a frame to the carrier; it does not wait for the remote receive. Affine means one live endpoint owner can advance a projected step at most once. The endpoint may be dropped, but it cannot be cloned or used to publish duplicate progress.
Hibana has two public surfaces:
Application code normally stays on hibana::g and Endpoint. Protocol
integration code uses hibana::runtime; it does not expose carrier state or
descriptor machinery to role code. docs.rs is the
signature reference for the same surface described here.
The temporary choreography value carries its structure in Rust while
project(&choreography) builds a compact RoleProgram<ROLE>. Endpoint futures
do not carry the choreography tree or every future payload type. Reusing one
projected artifact for many isolated sessions therefore does not multiply
endpoint types. Projection lowers the existing public DSL in one internal pass;
its flat event rows, scope markers, resolver markers, and allocation scratch do
not enter the endpoint, descriptor header, or Pico runtime state.
A named choreography can return impl Projectable, letting Rust infer its
step-list from the expression. These values compose through the same g
operators before projection; no second type-level declaration is required.
use hibana::{g, runtime::program::{Projectable, project}};
fn exchange() -> impl Projectable {
g::seq(
g::send::<0, 1, g::Msg<1, u32>>(),
g::send::<1, 0, g::Msg<2, u32>>(),
)
}
let conversation = g::seq(exchange(), exchange());
let client = project::<0>(&conversation);
let server = project::<1>(&conversation);Projectable is sealed: only Hibana choreography constructors establish it.
The unprojected value remains zero-sized, and composition preserves the concrete
step-list and projection checks. Runtime endpoints and owned resources are not
made copyable by this choreography interface.
Projection rejects unsupported route shapes, ambiguous simultaneous endpoint
operations, conflicting parallel lanes, empty parallel arms, and unguarded
re-entry. Logical message labels identify choreography messages; they need not
be globally unique. A same-role send is a zero-byte local effect and must use
(). It does not hide payload data in a private queue.
Repeated regions add no iteration field to endpoint types, descriptor rows, or the eight-byte core frame header. Freshness comes from the projected execution rules plus carrier FIFO, replay exclusion, and generation isolation, not from growing every frame or endpoint.
The compact descriptor domains impose these explicit limits:
Frame colors are not cumulative message numbers. More than 256 ordered
messages may reuse a color; distinct sources may also reuse a color because the
runtime compares source, lane, and frame color together. Inside .roll, equal
route paths reuse one color while distinct paths of the same inbound key receive
distinct colors for elastic re-entry. Projection rejects only a frontier that
genuinely requires a 257th color for one complete inbound key. Routes remain
binary by design.
The event-identity domain is not a promise that every 65,535-event source fits
one image. A protocol is accepted only when both its global image and every
projected role image fit their byte domains; the exact event ceiling therefore
depends on its messages, scopes, dependencies, route evidence, and role views.
The internal scope-id domain contains 8,192 identities, but this is not an
additional acceptance limit: even the smallest structured scope consumes ten
program-image bytes, so a fitting image contains at most 6,553 scopes. Route
commit-chain lengths use the same compact u16 count domain and are therefore
bounded by descriptor structure rather than by an unrelated 255-entry runtime
field. Runtime route history is a packed sparse table sized by emitted
(lane, route) relations, not by active lanes × maximum route depth.
The temporary source is still a Rust type tree, but lowering stores events,
normalized closed scope markers, and resolver markers in one exact-count tagged
arena. Scope publication is atomic, and primary markers carry the proof-only arm
boundaries needed by later passes; that metadata is erased from the descriptor.
Production const capacity validation ties source counts to the exact final
column counts and byte length, Kani checks the packed count domain, and Lean
proves generally that the exact descriptor bytes dominate the source-row count.
Row contents remain the separate responsibility of translation validation. The
temporary arena therefore has no smaller independent acceptance ceiling. Its
lane matching scratch is bounded by the 256-value wire lane domain rather than
by event count.
A const fixture constructs and emits the full 7,281-event
atom-only image. Public typed fixtures separately track 289 messages and 258
parallel events under rustc's default recursion limit. A Pico-target compile
gate projects 256 linear cyclic sender handoffs, 64 handoffs per route arm, and
a 64-event rolled cycle while bounding compiler time and memory for each causal
validation path. Large generated type trees should compose balanced subtrees;
genuinely nested source semantics deeper than that compiler limit may require a
crate-level recursion_limit. The dedicated >128 scope test keeps this source
constraint separate from runtime, descriptor, stack, and SRAM measurements.
Receive-lane sender changes use structured causal must analysis. A route joins only facts established in every possible arm; parallel arms start from the same incoming facts and cannot relay each other's intermediate results. A rolled body composes fresh visits with independent route choices. The exact 256-role fact set occupies 32 bytes of compiler scratch and adds no endpoint, wire, or runtime state. The Lean model proves must facts for every selected-arm execution and derives receive-before-send order under its explicit schedule premises. Generated kernel checks compare concrete Rust and Lean decisions; they are finite correspondence evidence, not a universal Rust refinement.
Role projection computes immutable source-to-parent scope facts once and shares those compiler facts across roles. The exact kind/ordinal domain is erased from the final descriptor. Route validation checks global authority once per scope and retains every role's observer checks. Parallel dependency compilation saves the shared sequential prefix at each fork, restores it at the split, and applies the whole local join after both arms. Both arms require that prefix even when the right arm introduces a new lane; neither arm acquires a dependency on its sibling's intermediate events. Shared-offset boundaries finish joins, restore splits, then record new inputs; serialized marker tie order is preserved. Initial offer dispatch follows the observed lane head when another arm has moved the shared cursor. Lean proves the sibling exclusion, retained sequential join, saved fork input, and lane-head preservation properties. Ten additional exact Rust/Lean descriptor fixtures and their corruption rejections are kernel-checked; these remain finite correspondence evidence rather than a universal Rust proof.
g::Msg<L, P> names logical label L and wire payload P. Built-in exact
codecs cover (), bool, signed and unsigned integers, byte slices, and fixed
byte arrays. Fixed-width decoders reject trailing bytes. Received slices may
borrow from the carrier-owned frame for the endpoint borrow.
Custom payloads implement both contracts:
- WireEncode::encode_intowrites deterministic bytes and reports their length;
- WirePayload::validate_payloadaccepts the exact canonical byte shape before endpoint progress commits;
- WirePayload::decode_validated_payloaddecodes bytes already validated;
- WirePayload::SCHEMA_IDnames that canonical wire contract in the descriptor.
The schema id is not a cross-binary Rust nominal type id and is not sent in the
core frame header. Incompatible encodings or validation rules require distinct
ids. Different Rust wrappers may share an id only when they deliberately
implement the same canonical bytes and validation. Schema 0 belongs to the
exact zero-byte unit schema.
This complete custom fixed-width codec illustrates the contract:
use hibana::runtime::wire::{CodecError, Payload, WireEncode, WirePayload};
struct FourBytes([u8; 4]);
impl WireEncode for FourBytes {
fn encode_into(&self, out: &mut [u8]) -> Result<usize, CodecError> {
if out.len() < 4 {
return Err(CodecError::Truncated);
}
out[..4].copy_from_slice(&self.0);
Ok(4)
}
}
impl WirePayload for FourBytes {
const SCHEMA_ID: u32 = 0x4000_0000;
type Decoded<'a> = FourBytes;
fn validate_payload(input: Payload<'_>) -> Result<(), CodecError> {
if input.as_bytes().len() == 4 {
Ok(())
} else {
Err(CodecError::Malformed)
}
}
fn decode_validated_payload(input: Payload<'_>) -> Self::Decoded<'_> {
let bytes = input.as_bytes();
FourBytes([bytes[0], bytes[1], bytes[2], bytes[3]])
}
}Codec correctness remains the codec implementor's responsibility. Hibana checks that each operation uses the schema id projected for that event and that the decoder accepts the received bytes before committing progress.
The role API is deliberately small:
Inside an async role function, ordinary message flow is direct:
use hibana::{Endpoint, EndpointError, g::Msg};
async fn client(endpoint: &mut Endpoint<'_, 0>) -> Result<u16, EndpointError> {
let request = [1, 2, 3, 4];
endpoint.send::<Msg<10, [u8; 4]>>(&request).await?;
endpoint.recv::<Msg<11, u16>>().await
}Endpoint progress happens when send(), recv(), or a route branch first-step
operation succeeds. Dropping an unpolled send publishes no progress. A dropped
route preview, rejected operation, or successful requeue(...) consumes no
protocol step.
Prefer in-band choice: make the message that selects a branch its first visible
action. RouteBranch::label() then reports that selected arm's first logical
message label, and the first send or receive is performed through the branch.
Payload contents, queue position, and carrier observations are never branch
authority.
For example, this route is selected by the first message visible to role 1:
use hibana::g;
let accepted = g::send::<0, 1, g::Msg<31, u32>>();
let rejected = g::send::<0, 1, g::Msg<33, ()>>();
let routed = g::route(accepted, rejected);The receiving role previews, inspects, and consumes that selected first step:
use hibana::{Endpoint, EndpointError, g::Msg};
async fn receive_choice(
endpoint: &mut Endpoint<'_, 1>,
) -> Result<Option<u32>, EndpointError> {
let branch = endpoint.offer().await?;
match branch.label() {
31 => Ok(Some(branch.recv::<Msg<31, u32>>().await?)),
33 => {
branch.recv::<Msg<33, ()>>().await?;
Ok(None)
}
label => panic!("unexpected route label {label}"),
}
}When a timer, readiness signal, budget, or another non-message signal owns the
choice, mark the route with .resolve::<ID>() and install a typed
ResolverRef::<ID>::decision_state(...). Resolver failure rejects the step; it
does not select another arm. Resolver state is local input, so roles that act
before receiving in-band branch evidence need deployment-level agreement on
the decision.
g::par(left, right) combines independent flows. Projection assigns logical
lanes and rejects simultaneous local operations that cannot be selected
exactly. The arms are not threads and do not choose an executor; they describe
protocol independence that the attached roles may drive concurrently.
use hibana::g;
let left = g::send::<0, 1, g::Msg<50, u32>>();
let right = g::send::<2, 3, g::Msg<50, u32>>();
let independent = g::par(left, right);.roll() marks a guarded structural region that may re-enter. For an explicit
route resolver, resolve the route first and roll the surrounding region second:
use hibana::g;
const ROUTE_DECISION: u16 = 7;
let repeated = g::route(
g::send::<0, 1, g::Msg<40, u32>>(),
g::send::<0, 1, g::Msg<41, ()>>(),
)
.resolve::<ROUTE_DECISION>()
.roll();The reverse call order is unavailable because resolve::<ID>() belongs to a
route value, not to the rolled result. Nested repeated regions follow the same
rule. An intentional infinite repeated region is valid protocol behavior, so
Hibana does not claim that every session terminates.
The runtime borrows one caller-provided byte region and derives its internal
layout from the projected descriptors. SessionKitStorage::uninit().init() is
the single construction path. SessionKit::rendezvous(...) binds the storage
region and one transport. RendezvousKit::enter(...) attaches a projected role
to a session.
SessionKit and its endpoints belong to one local runtime owner; they are not
shared concurrent handles. Interrupts, worker threads, and device callbacks
communicate through transport-owned state and wake the executor through stored
wakers. The executor itself is integration-owned.
The runnable example uses this complete construction sequence after projection:
use hibana::runtime::{SessionKitStorage, ids::SessionId};
let mut slab = [0_u8; 3 * 1024];
let mut storage = SessionKitStorage::<InMemoryTransport>::uninit();
let kit = storage.init();
let rendezvous = kit
.rendezvous(&mut slab, InMemoryTransport::new())
.expect("create rendezvous");
let session = SessionId::new(1);
let client = rendezvous
.enter(session, &client_program)
.expect("attach client");
let server = rendezvous
.enter(session, &server_program)
.expect("attach server");InMemoryTransport, client_program, and server_program are defined by the
runnable example. A deployment replaces only the transport and measured slab
budget. SessionKitStorage, the choreography, projection, attach sequence, and
endpoint API are unchanged. An undersized slab produces AttachError; Hibana
does not substitute a smaller layout or hidden allocation.
The first local attach binds a session generation to one exact compiled
program image. A byte-different image or a second live attach for the same
(rendezvous, SessionId, role) is rejected. Dropping an endpoint releases its
lease. Resolver-dependent local roles must be attached before first resolver
execution seals local membership.
Transport owns byte buffers, framing, readiness, ingress demultiplexing, and
wakeups. Hibana owns choreography meaning and route authority. Transport
implementations provide two associated handle types and five operations:
PortOpen exposes local_role(), session_id(), and lane(). Outgoing
exposes frame_label(), target_role(), lane(), and payload(). The handles
returned by open may borrow buffers, device state, DMA records, and wakers
from the transport owner, so no allocation or transport-specific future type
enters Hibana's endpoint API.
After poll_send returns Pending, a later poll supplies the same encoded
content again, but its scratch address may differ. The transport may retain its
own progress in Tx; it must not retain the prior Payload pointer.
Receive evidence has two explicit construction paths:
use hibana::runtime::{
transport::{FrameHeader, ReceivedFrame},
wire::Payload,
};
let direct = ReceivedFrame::deterministic(Payload::new(payload_bytes));
let framed = ReceivedFrame::framed(
FrameHeader::from_bytes(header_bytes),
Payload::new(payload_bytes),
);ReceivedFrame::deterministic(...) is valid only when direct recv() has one
live descriptor, or after RouteBranch::recv() already owns one materialized
receive descriptor. Route offer and unresolved route demultiplexing require
ReceivedFrame::framed(...) evidence. The core header is exactly eight
carrier-owned bytes:
session id (4 bytes, big endian) | lane | source role | target role | frame label
The transport stores the PortOpen facts needed to build or validate that
framing. A framed receive is checked against the endpoint's exact session, lane,
source, target, frame label, descriptor event, logical label, and schema before
progress commits. A deterministic receive does not claim to observe source,
target, or frame label: its lane-bound Rx handle plus the requested logical label
and schema must identify exactly one enabled descriptor receive. Zero or multiple
matches fail closed. Peer authenticity and affine delivery remain carrier-profile
premises in both cases; reordering, repetition, and mismatch are not repaired
into ordinary progress.
A successful poll_send proves carrier acceptance, not remote receipt. To lift
local enforcement to global fidelity and progress, a concrete carrier must
also provide:
- expected peer and direction binding;
- FIFO delivery within each mapped logical direction;
- no unsolicited replay and no frame leakage across carrier generations;
- exactly one observation for each delivered frame;
- eventual delivery of accepted frames or observable terminal closure;
- receiver wakeup after accepted frames drain or are quarantined on closure.
Fresh transport-instance state is a sufficient carrier generation. Address or
path changes may remain inside one generation. Reusing a SessionId after
retirement requires carrier state that cannot expose a frame from the retired
generation. A multiplexed carrier may retire one logical direction while
unrelated sessions remain live.
Route agreement also requires every controller to execute its accepted image through its Endpoint. Passive endpoints cannot detect a controller that bypasses the kernel and fabricates opposite-arm frames for different peers. Peer authentication alone does not make such a controller conforming. Hibana does not implement Byzantine agreement between independent passive endpoints; the carrier must preserve provenance from the conforming sender execution.
Protocol-invisible liveness detection belongs to the transport. A wait that
cannot progress returns TransportError from poll_send or poll_recv; it
does not create a hidden timeout branch. Returning Pending forever after
known peer closure does not satisfy the closing contract.
Hibana does not require an in-band protocol-image handshake. A deployment may establish exact role-image agreement through its build artifact, authenticated manifest, or an application protocol. This keeps bootstrap policy out of the core and permits carriers with different framing requirements.
The Unix datagram carrier is an executable conformance example for peer binding, FIFO delivery, replay exclusion, closure wakeup, and generation isolation. It demonstrates that the contract is realizable; it is not a mandatory dependency or universal proof of third-party transports.
An explicit resolver connects a non-message decision owner to a route marked
with .resolve::<ID>(). The id is checked against the projected role program,
and the state reference lives for the runtime configuration lifetime.
use hibana::runtime::resolver::{DecisionArm, ResolverError, ResolverRef};
const ROUTE_RESOLVER: u16 = 7;
struct RouteState {
accept: bool,
}
fn decide_route(state: &RouteState) -> Result<DecisionArm, ResolverError> {
if state.accept {
Ok(DecisionArm::Left)
} else {
Ok(DecisionArm::Right)
}
}
let state = RouteState { accept: true };
let resolver = ResolverRef::<ROUTE_RESOLVER>::decision_state(&state, decide_route);
rendezvous.set_resolver(&role_program, resolver)?;Register against the exact RoleProgram that contains the resolver site.
ResolverRef::decide() permits typed resolver owners to compose other typed
resolver owners without exposing erased storage. Resolver rejection is
terminal evidence for that attempted endpoint step and never grants alternate
route authority.
A resolver registered in one rendezvous does not establish agreement with a remote device. If several roles act before receiving an in-band indication, the deployment or application protocol must supply the same decision to those resolver owners.
A projected descriptor is a finite session template, not a singleton runtime
instance. Distinct SessionId values have independent cursors, queues, leases,
and failure domains. Resolver registrations belong to the exact role program
within one rendezvous and may deliberately read application state shared across
sessions. Retrying an interaction or changing the finite participant set
creates a fresh session; changing the choreography also creates a fresh
projected artifact.
Persistent application data, membership policy, scheduling, restart policy, and algorithm invariants remain application-owned. Larger systems may compose explicit families of finite sessions, but each session keeps its own protocol guarantee. This is an application architecture, not an equivalent encoding of one global choreography across those sessions.
RendezvousKit::tap() returns a read-only iterator over the latest 21 public
16-byte evidence values. The ring stores 12-byte records and rebuilds their
monotonic timestamps while reading, so its 252-byte storage stays within the
256-byte budget. Events cover endpoint operations, carrier observations,
faults, lanes, route selection, and resolver decisions. Public code may read
records but cannot construct or push them. Tap is diagnostic evidence; it
cannot select a route or authorize progress.
Each public boundary reports its own error instead of widening all failures into one catch-all type:
EndpointError is terminal diagnostic evidence for the current session
generation. A codec mismatch, descriptor mismatch, or carrier failure poisons
that generation and wakes local waiters. Remote cancellation termination also
requires the carrier to make peer closure observable after accepted frames are
drained or quarantined.
There is no public same-generation retry, reselection, timeout, or cancellation operation. Errors are not route arms. A fresh attempt uses a fresh session generation; a protocol-visible timeout or cancellation is expressed as an ordinary choreography message or explicit route decision.
For every attached endpoint, Hibana enforces:
- exactly one permitted descriptor transition for each successful operation;
- zero transitions for previews, rejection, drop before commit, and requeue;
- fail-closed checks of peer, direction, lane, event, label, schema, and payload;
- no duplicate publication by one endpoint owner;
- first-fault preservation and terminal local waiter wakeup;
- isolation between live SessionIdgenerations in one runtime.
project(&choreography) rejects unsupported or ambiguous choreographies. The
machine-checked global theorems apply to exact role images accepted by the
independent protocol artifact checker.
These guarantees do not silently absorb external responsibilities:
Successful projection alone is not a distributed deadlock-freedom guarantee. Hibana provides per-session protocol deadlock freedom when all of the following hold:
- every role executes the exact accepted image of the same projectable choreography;
- peers agree on each canonical wire schema and use conforming codecs;
- the carrier binds the expected peers and directions, preserves FIFO order, excludes replay across session generations, and eventually delivers each accepted frame or reports terminal closure;
- the executor eventually polls operations that remain enabled.
Under those conditions, every reachable live, unfinished protocol state has an
enabled transition. An intentional infinite .roll may continue forever, and
application cycles spanning separate sessions remain application scheduling
concerns.
The repository compiles the public choreography and projection API for
thumbv6m-none-eabi without an allocator, SDK, host transport, or target-only
Hibana API. The release gate publishes fresh measurements for each checked
revision and enforces the tracked resource ceilings. Measured values are not
copied into a manually synchronized source table here.
The gate measures SessionKitStorage, fixed per-session storage including tap
records, peak live runtime slab, operation stack, modeled SRAM, the minimal
and largest linked protocol artifacts, and complete library sections.
For example, the dafdf8a CI measurement
reported a 5,274 B modeled runtime SRAM envelope and a 2,591 B operation-stack
high-water mark, within the unchanged 8,954 B and 3,663 B ceilings. These are
revision-specific observations, not promises for arbitrary application state.
The no-default thumbv6m-none-eabi rlib sections were 97,344 B, below the
169,965 B ceiling. A complete rlib is not the flash cost paid by one linked
protocol. Host stack observations use the pinned
aarch64-unknown-linux-gnu measurement host.
The modeled SRAM envelope combines the target's Hibana .data/.bss, storage
owners, one measured live slab shape, and runtime operation stack. Component
maxima may come from different shapes and must not be added as one observed
run. Application state, concrete transport buffers, executor state, interrupt
stacks, codec scratch, and platform startup are outside this Hibana-owned
envelope.
examples/pico/src/lib.rs is the tracked no_std
projection sample. The release gate regenerates these measurements and rejects
any value above its ceiling.
Hibana uses complementary tools rather than attributing every guarantee to one checker:
The Lean verification guide summarizes the checked boundary, assumptions, generated artifacts, and machine-checked claim inventories. Each tool is evidence only for the part it checks. Kani and Miri strengthen the Rust implementation evidence; neither is presented as a Lean proof of arbitrary Rust source.
The static Lean theorem package and exact descriptor/kernel certificates are kernel-checked. Finite executable regressions and concrete finite-closure witnesses that use the pinned native evaluator are isolated and audited rather than presented as kernel-only proofs.
Release gates discover the Lean, Kani, and Miri inventories from their canonical sources, pin Lean claim types and axiom closures, and reject missing or changed obligations. Current inventory counts are emitted by the gates instead of being duplicated in documentation.
The crate has no normal dependencies and no feature-selected host API. Useful checks from a repository checkout are:
cargo +1.95.0 check --no-default-features --lib -p hibana
cargo +1.95.0 test -p hibana --test ui
cargo +1.95.0 clippy --all-targets -- -D warnings
cargo +1.95.0 doc -p hibana --no-deps --no-default-featuresCompile the tracked embedded projection with the same public API:
rustup target add --toolchain 1.95.0 thumbv6m-none-eabi
cargo +1.95.0 check --manifest-path examples/pico/Cargo.toml \
--target thumbv6m-none-eabiRun the complete non-Kani release gate with the pinned toolchains:
bash ./.github/scripts/run_final_form_gates.shIt executes the runnable example, Rust tests, no_std target checks, rustdoc,
package checks, Miri, Lean, the Unix carrier conformance suite, and resource
measurements. Rust tests exercise protocol behavior and compile-time ownership;
resource gates measure compiled artifacts and operation stack use. Package
checks compile the extracted crate and its test modules. CI leaves internal
names, file layout and documentation wording to code review. Kani/CBMC is a
separate required CI job and can be run locally
after installing the version recorded in .github/kani-version:
bash ./.github/scripts/check_kani.shHibana covers finite-role sessions executed through its endpoint API. It does not claim correctness for code that bypasses the endpoint, arbitrary transport implementations, application algorithms, carrier authentication or cryptography, failure-detector accuracy, unbounded role sets, or channel delegation. Cross-binary agreement is defined over canonical wire schemas, not Rust nominal type identity.
The exact public position is therefore: a compact choreography-derived runtime enforcement kernel for finite-role affine asynchronous multiparty protocols, with distributed fidelity, progress, and cancellation conclusions stated under explicit carrier, deployment, codec, and scheduling requirements.
Hibana is licensed under either Apache-2.0 or MIT, at your option.
Projection errors identify the affected role, structured scope, arm event ranges,
and source messages when a witness is available. For example, a receive-lane
error can name event#0(8->9 label=168 lane=0) followed by
event#1(27->9 label=190 lane=0) and request a causal handoff. A rolled error also
identifies the reentry scope. Missing branch knowledge names the passive role
and shows which arm has no local event.
For a read-only structured explanation without constructing endpoints, call
g::diagnose(&program). It returns Option<g::ProjectionDiagnostic> and supports
Display and Debug. None means the existing projection checks accept; it is
not evidence about payload algorithms or physical I/O. Projection itself remains
fail-closed and includes the available explanation in its compile-time error.
Scope and event numbers are zero-based source-order ordinals, not Rust line
numbers. Some selector/passive-child failures currently have only a category;
missing witnesses are never guessed. See proofs/projection-diagnostics for the
verification scope and regression checks.
For finite RX/TX completion, failure, and resource-return boundaries using the existing API, see the executable explicit-resource-join example and verification. This preserves independent emergency stop and long-running parallel loops; it adds no automatic native-resource guarantee.