Hibana: Runtime Enforcement for Choreographic Programming in Rust

Hibana is a specialized runtime enforcement kernel designed for Rust. It allows developers to execute complex, multiparty protocols derived from a single, global choreography.

By projecting a global choreography into streamlined programs for each participating role, Hibana ensures that every send, receive, or route operation is validated against the projected program before any progress is committed.

---

🛠 Technical Architecture

Hibana is engineered for maximum efficiency and portability:

• Environment: It is unconditionally no_std.
• Memory: It requires no dynamic allocator $\rightarrow$ zero allocation, relying instead on storage provided by the caller.
• State Management: Rather than creating a unique Rust continuation type for every possible state (which would lead to "type explosion"), protocol state is managed via compact descriptors.

Core Capabilities

System Flow

---

⚠️ Scope and Boundaries

It is important to understand what Hibana is and is not:

• Enforces the protocol at each attached endpoint.
• Defines the necessary conditions (carrier, codec, scheduling) to achieve distributed guarantees.
• Implements a network stack.
• Implements distributed algorithms.

Note on Sessions: If a protocol is split across multiple sessions, the guarantee boundary shifts. Hibana validates each session individually rather than treating the entire set as one global protocol.

---

📖 Documentation Roadmap

The project is organized by the following responsibilities:

1. The Model: Understanding enforcement, external dependencies, and state compactness.
2. Writing Choreographies: Using the Protocol Language for messages, routes, and parallel flows.
3. Implementing Roles: Handling send, recv, offer, and branching.
4. Protocol Integration: Managing the runtime boundary, storage, and resolvers.
5. Carrier Implementation: Fulfilling the Transport trait's five-operation contract.
6. Deployment Auditing: Verifying resource usage and local/distributed guarantees.

---

🚀 Quick Start

Installation

Add the dependency to your project: cargo add hibana

Requirements: Rust 2024 edition, stable Rust 1.95+.

Example: Ping-Pong

To run the built-in example: cargo run --example ping_pong ping=7, pong=8

The Protocol Logic

The following snippet demonstrates how a simple choreography is defined and projected:

use hibana::{
    g::{self, Msg},
    runtime::program::{RoleProgram, project},
};

fn ping_pong() -> (RoleProgram<0>, RoleProgram<1>) {
    // Define a sequential flow: 0 sends to 1, then 1 sends to 0
    let choreography = g::seq(
        g::send::<(0, 1), Msg::Msg1, u32>(), 
        g::send::<(1, 0), Msg::Msg2, u32>(),
    );
    
    // Project the global choreography into role-specific programs
    (project(choreography), project(choreography))
}

In a real execution, the developer provides the runtime storage and a Transport implementation (e.g., in-memory for tests), attaches roles to a SessionId, and drives the logic via send() and recv().

---

🧠 The Conceptual Model

The Lifecycle

$\text{Global Choreography} \rightarrow \text{project()} \rightarrow \text{RoleProgram} \rightarrow \text{SessionId} \rightarrow \text{Endpoint Ops} \rightarrow \text{Commit/Fail}$

Key Definitions

• Multiparty: The identity of the peer, the direction of flow, and the sequence of events are all derived from the single projected choreography.
• Asynchronous: A send operation is considered successful once the frame is handed to the carrier; it does not block for the remote party's receive.
• Affine: An endpoint owner can advance a projected step exactly once. While the endpoint can be discarded (dropped), it cannot be duplicated.

Public API Surfaces

Application logic typically interacts only with the Audience Surface, while the Integration Surface handles the underlying machinery without exposing carrier state to the role code.

Efficiency Note

The choreography structure exists as a temporary Rust value. Once project(choreography) is called, it is converted into a compact RoleProgram. Consequently, Endpoint futures do not need to store the entire choreography tree or every possible payload type, ensuring that reusing a projected artifact across many sessions does not lead to a proliferation of endpoint types.