Enum SessionType 

pub enum SessionType {
    End,
    Send {
        payload: Payload,
        credit: Option<u64>,
        cont: Box<SessionType>,
    },
    Recv {
        payload: Payload,
        credit: Option<u64>,
        cont: Box<SessionType>,
    },
    Select(BTreeMap<String, SessionType>),
    Branch(BTreeMap<String, SessionType>),
    Rec(String, Box<SessionType>),
    Var(String),
}

A session type — the protocol of one endpoint of a connection (§3.1 of the paper). Select/Branch carry their labelled continuations in a BTreeMap so the label set is canonically ordered (deterministic duality + equality).

Serialize + Deserialize — §Fase 41.g sealed-snapshot resume needs the residual cursor + the protocol schema serialisable. The encoding is stable across the algebra layer + the enterprise persistence layer: the same JSON shape goes into the AAD-bound cognitive_states ciphertext and comes back out via [SessionRuntime::resume].

Variants

End

end — the dialogue is complete.

Send

!ⁿA.S — send a value of type A, then behave as S. The optional credit is the Fase 41.c index n (paper §4.2): Some(n) types a send that requires n > 0 available credit (the “no rule at n = 0” axiom makes Some(0) unprovable); None is the unbounded fragment !∞A.S.

Fields

payload: Payload

credit: Option<u64>

cont: Box<SessionType>

Recv

?ⁿA.S — receive a value of type A, then behave as S. Symmetric to SessionType::Send: the index n bounds the receiver-side window.

Fields

payload: Payload

credit: Option<u64>

cont: Box<SessionType>

Select(BTreeMap<String, SessionType>)

⊕{ℓᵢ:Sᵢ} — internal choice: this endpoint selects a label.

Branch(BTreeMap<String, SessionType>)

&{ℓᵢ:Sᵢ} — external choice: this endpoint offers the branches.

Rec(String, Box<SessionType>)

μX.S — recursive session (equirecursive: μX.S ≡ S[μX.S/X]).

Var(String)

X — a recursion variable (bound by an enclosing Rec).

Implementations

impl SessionType

pub fn send(payload: impl Into<String>, then: SessionType) -> SessionType

!A.S — unbounded send (credit = None, the pre-41.c fragment).

pub fn recv(payload: impl Into<String>, then: SessionType) -> SessionType

?A.S — unbounded receive (credit = None).

pub fn send_credit( payload: impl Into<String>, n: u64, then: SessionType, ) -> SessionType

!ⁿA.S — credit-refined send (Fase 41.c, paper §4.2). The continuation then runs in the same window — the budget is global to the socket; the n here is the snapshot of available credit demanded at this step.

pub fn recv_credit( payload: impl Into<String>, n: u64, then: SessionType, ) -> SessionType

?ⁿA.S — credit-refined receive (Fase 41.c).

pub fn select( branches: impl IntoIterator<Item = (String, SessionType)>, ) -> SessionType

pub fn branch( branches: impl IntoIterator<Item = (String, SessionType)>, ) -> SessionType

pub fn rec(var: impl Into<String>, body: SessionType) -> SessionType

pub fn var(name: impl Into<String>) -> SessionType

pub fn dual(&self) -> SessionType

The dual S⊥: swaps send↔recv and select↔branch, recursing into continuations; end, Rec binders and Vars are preserved. Payloads and the credit index n are unchanged — (!ⁿA.S)⊥ = ?ⁿA.S⊥ (same A, same n, opposite direction). Symmetric credit is the standard credit-flow semantics (Rast lineage): the sender’s window-of-n is exactly what the receiver-side is sized to absorb.

pub fn unfold_head(&self) -> SessionType

Unfold every leading Rec so the head constructor is exposed: μX.S ↦ S[μX.S/X], repeated. Terminates for contractive types (a guard appears under each Rec before the variable recurs).

Public so the 41.d runtime can drive the session-type cursor over a live connection: after every operational step the continuation is re-unfolded so the cursor never carries a leading Rec for the state machine to interpret.

pub fn equiv(&self, other: &SessionType) -> bool

Equirecursive equality: S ≡ T iff their infinite unfoldings coincide. Decided by the standard coinductive algorithm — assume the pair equal, unfold leading Recs, compare heads, recurse; a re-encountered pair is discharged by the assumption (the greatest fixed point). Terminates because a regular type has finitely many distinct sub-pairs.

pub fn is_dual_to(&self, peer: &SessionType) -> bool

The connection law (§3.2): a connection whose two endpoints are typed self and peer is well-formed iff peer ≡ self⊥. Symmetric up to involutivity ((S⊥)⊥ ≡ S).

pub fn with_credit(&self, n: u64) -> SessionType

Stamp every (recursively-reachable) Send and Recv with the credit index n. Idempotent on already-stamped types. Used by the type checker to lift the socket’s backpressure: credit(k) annotation onto the bare session protocol so the algebra-level analysis can discharge the constraint.

pub fn has_send_at_zero(&self) -> Option<Payload>

The “no rule at n = 0” axiom (paper §4.2): an explicit !⁰A.S in the type is unprovable — there is no typing rule for a send at zero available credit. Returns the offending payload of the first such send (in a deterministic left-to-right walk) if any.

Decidable in linear time over the type structure.

pub fn credit_analyse(&self, budget: u64) -> Result<(), CreditError>

Decide the credit conformance of self against a budget k (the socket’s backpressure: credit(k) window). This is the Presburger discharge — the constraints are linear arithmetic over the naturals, so satisfiability is decidable; the algorithm here is the direct fixpoint formulation specialised to closed, contractive session types (Rast lineage, §4.2 of the paper).

The check fires three kinds of error:

1. Send at zero — an explicit !⁰A.S in the type. Unprovable by construction (no typing rule applies).
2. Burst overflow — a straight-line send burst exceeding the available window. With initial budget k, the abstract trace must never reach available_credit < 0 at a send.
3. Loop unsustainability — a recursive body whose per-iteration net send count Δ = #send − #recv is strictly positive: each iteration drains the window, so unbounded iteration is unsound under any finite budget. (Δ ≤ 0 is the Presburger fixpoint inequality.)

Returns Ok(()) if the protocol is conformant, or CreditError with the offending witness. Total over closed, contractive session types.

pub fn recurring_paths(&self, x: &str) -> Vec<(u64, u64)>

Enumerate the recurring paths of self w.r.t. recursion variable x — every trace from the root that reaches Var(x). Each path is reported as (#send, #recv); terminating paths (reaching End or a different free variable) are dropped (they don’t iterate, so they don’t constrain unbounded sustainability). Shadowing Rec(x, …) cuts the descent — references inside refer to the inner binder.

Total in time linear in the size of self; the path count is bounded by the number of leaves of the choice tree.

pub fn credit_delta(&self, x: &str) -> (u64, u64)

Worst-case (maximum-Δ) recurring path of self w.r.t. x. Used by the type checker to report the offending iteration count. Returns (0, 0) if there are no recurring paths.

pub fn projects_to_sse(&self) -> bool

True iff self lies in the SSE producer fragment: the connection only sends to its peer. Concretely the type contains only End, Send, internal-Select, Rec, and Var — no Recv (would mean the producer expects client input) and no Branch (would mean the producer offers a choice the client picks). For such a type the §4.4 identity S_SSE = Π↓(S_WS) holds with Π↓ = id: the protocol is already the SSE fragment, runnable over W3C SSE without WebSocket bidirectionality.

Total over closed, contractive session types; linear in the size of self.

pub fn projects_to_sse_consumer(&self) -> bool

Dual of [projects_to_sse] — the SSE consumer fragment: the connection only receives from its peer (End, Recv, external-Branch, Rec, Var). The §4.4 theorem Π↓(S)⊥ = Π↑(S⊥) ties this to projects_to_sse via duality: S.projects_to_sse() ⇔ S.dual().projects_to_sse_consumer().

pub fn has_polarity(&self, p: Polarity) -> bool

Unified polarity test. The two SSE fragments are exactly the two inhabitants of Polarity: Producer = !/⊕/end/μ/var-only and Consumer = ?/&/end/μ/var-only.

Trait Implementations

impl Clone for SessionType

fn clone(&self) -> SessionType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SessionType

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SessionType

fn deserialize<__D>( __deserializer: __D, ) -> Result<SessionType, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for SessionType

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Eq for SessionType

impl Hash for SessionType

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for SessionType

fn eq(&self, other: &SessionType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for SessionType

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for SessionType