Module session 

Session types for protocol-safe communication.

Session types encode communication protocols at the type level, ensuring protocol compliance at compile time. This module provides:

• Core protocol building blocks: Send, Recv, Choose, Offer, End
• Duality: Every session type has a dual — if one endpoint sends, the other receives
• Typed endpoints: Communication channels that advance through protocol states

Protocol Example

A simple request-response protocol:

// Client side: send a request, receive a response
type ClientProtocol = Send<Request, Recv<Response, End>>;

// Server side is the dual: receive a request, send a response
type ServerProtocol = Dual<ClientProtocol>;
// = Recv<Request, Send<Response, End>>

Design

Session types are zero-sized marker types that exist only at compile time. They encode the protocol as a type-level state machine. Each communication operation consumes the current endpoint and returns one at the next state, ensuring protocol steps are followed in order and exactly once (affine use).

Compile-Time Protocol Compliance

Protocol violations are type errors. The following shows correct usage:

use asupersync::session::{Send, Recv, End, Session, Dual};

// Dual of Send<T, End> is Recv<T, End>
fn _check_duality() {
    fn _assert_same<A, B>() where A: Session<Dual = B>, B: Session<Dual = A> {}
    _assert_same::<Send<u32, End>, Recv<u32, End>>();
}

Attempting to call send on a Recv endpoint is a type error:

use asupersync::session::{Recv, End, channel};

// ERROR: Endpoint<Recv<u32, End>> does not have a send() method
async fn wrong_direction() {
    let cx = asupersync::cx::Cx::for_testing();
    type P = Recv<u32, End>;
    let (ep, _peer) = channel::<P>();
    ep.send(&cx, 42).await.unwrap();
}

Attempting to close an endpoint before the protocol completes is a type error:

use asupersync::session::{Send, End, channel};

// ERROR: Endpoint<Send<u32, End>> does not have close()
fn premature_close() {
    type P = Send<u32, End>;
    let (ep, _peer) = channel::<P>();
    ep.close(); // Only Endpoint<End> has close()
}

Calling recv on a Send endpoint is a type error:

use asupersync::session::{Send, End, channel};

// ERROR: Endpoint<Send<u32, End>> does not have recv()
async fn recv_on_send() {
    let cx = asupersync::cx::Cx::for_testing();
    type P = Send<u32, End>;
    let (ep, _peer) = channel::<P>();
    ep.recv(&cx).await.unwrap();
}

Obligation Protocol Facade

The obligation submodule is the public facade for the obligation-backed typestate protocols shipped in crate::obligation::session_types. Keep the two surfaces distinct:

Use this surface	When
channel plus Endpoint	You need a general binary session channel for an application protocol.
obligation::send_permit	You are proving the two-phase reserve/send-or-abort protocol.
obligation::lease	You are proving acquire/renew/release resource ownership.
obligation::two_phase	You are proving reserve/commit-or-abort effects.
crate::obligation::choreography	You need a global choreography DSL; code generation remains an obligation-module surface.

The obligation facade is not exported through a prelude. Session protocols encode linear state transitions, so callers should import the exact protocol they are driving.

The API surface map already records the root crate::session module as the public entry point; these protocol modules are nested under that entry.

Choreography disposition: crate::obligation::choreography remains an experimental obligation-module surface. The global-protocol builder is useful for documenting and validating choreographies, but the projection/codegen path is still separate from this facade, so it is intentionally not re-exported as session::obligation::*.

Negative-space compile-fail examples live alongside the implementation in crate::obligation::session_types. They prove that out-of-order sends, premature closes, and late aborts fail at compile time.

SendPermit commit path:

use asupersync::session::obligation::{Branch, Selected, send_permit};

let (sender, receiver) = send_permit::new_session::<u64>(100);

let sender = sender.send(send_permit::ReserveMsg);
let sender = sender.select_left();
let sender = sender.send(42);
let sender_proof = sender.close();

let (_, receiver) = receiver.recv(send_permit::ReserveMsg);
let receiver_proof = match receiver.offer(Branch::Left) {
    Selected::Left(channel) => {
        let (value, channel) = channel.recv(42);
        assert_eq!(value, 42);
        channel.close()
    }
    Selected::Right(_) => panic!("expected send branch"),
};

assert_eq!(sender_proof.channel_id, receiver_proof.channel_id);

Lease release path:

use asupersync::session::obligation::{Branch, Selected, lease};

let (holder, resource) = lease::new_session(200);

let holder = holder.send(lease::AcquireMsg);
let holder = holder.select_right();
let holder = holder.send(lease::ReleaseMsg);
let holder_proof = holder.close();

let (_, resource) = resource.recv(lease::AcquireMsg);
let resource_proof = match resource.offer(Branch::Right) {
    Selected::Right(channel) => {
        let (_, channel) = channel.recv(lease::ReleaseMsg);
        channel.close()
    }
    Selected::Left(_) => panic!("expected release branch"),
};

assert_eq!(holder_proof.channel_id, resource_proof.channel_id);

Two-phase commit path:

use asupersync::record::ObligationKind;
use asupersync::session::obligation::{Branch, Selected, two_phase};

let kind = ObligationKind::IoOp;
let (initiator, executor) = two_phase::new_session(300, kind);
let reserve = two_phase::ReserveMsg { kind };

let initiator = initiator.send(reserve.clone());
let initiator = initiator.select_left();
let initiator = initiator.send(two_phase::CommitMsg);
let initiator_proof = initiator.close();

let (received, executor) = executor.recv(reserve);
assert_eq!(received.kind, kind);
let executor_proof = match executor.offer(Branch::Left) {
    Selected::Left(channel) => {
        let (_, channel) = channel.recv(two_phase::CommitMsg);
        channel.close()
    }
    Selected::Right(_) => panic!("expected commit branch"),
};

assert_eq!(initiator_proof.obligation_kind, executor_proof.obligation_kind);

Modules

obligation

Public facade for obligation-backed session protocols.

Structs

Choose

A protocol step where this endpoint chooses between two continuations.

End

Protocol termination — no further communication.

Endpoint

A typed endpoint at session state S.

Offer

A protocol step where this endpoint offers two continuations for the peer to choose.

Recv

A protocol step that receives a value of type T, then continues with Next.

Send

A protocol step that sends a value of type T, then continues with Next.

Enums

Branch

Direction chosen by Choose — left or right branch.

Offered

Result of an offer operation — the peer’s chosen branch.

SessionError

Error returned when a session operation fails.

Traits

Session

Marker trait for valid session types.

Functions

channel

Creates a pair of dual session-typed endpoints.

Type Aliases

Dual

Computes the dual of a session type.