telltale_machine/session/
overview.rs

1// Session lifecycle and store.
2//
3// Matches the Lean `SessionState`, `SessionStore` from `lean/Runtime/ProtocolMachine/Model/State.lean`.
4// Local type state lives here — the session store is the single source
5// of truth for per-endpoint type advancement.
6
7/// Archival summary for a closed session that has been reaped from live state.
8#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
9pub struct ClosedSessionSummary {
10    /// Session identifier.
11    pub sid: SessionId,
12    /// Terminal session status at reap time.
13    pub status: SessionStatus,
14    /// Number of participant roles.
15    pub role_count: usize,
16    /// Number of retained endpoint type entries at reap time.
17    pub local_type_entries: usize,
18    /// Number of directed edges tracked by the session.
19    pub edge_count: usize,
20    /// Number of edge-bound handlers.
21    pub edge_handler_count: usize,
22    /// Number of accumulated auth leaves across all edges.
23    pub auth_leaf_count: usize,
24    /// Number of auth trees retained by the session.
25    pub auth_tree_count: usize,
26    /// Number of auth roots retained by the session.
27    pub auth_root_count: usize,
28    /// Final epoch value.
29    pub epoch: usize,
30}
31
32impl ClosedSessionSummary {
33    fn from_session(session: &SessionState) -> Self {
34        Self {
35            sid: session.sid,
36            status: session.status.clone(),
37            role_count: session.roles.len(),
38            local_type_entries: session.local_types.len(),
39            edge_count: session.buffers.len(),
40            edge_handler_count: session.edge_handlers.len(),
41            auth_leaf_count: session.auth_leaves.values().map(Vec::len).sum(),
42            auth_tree_count: session.auth_trees.len(),
43            auth_root_count: session.auth_roots.len(),
44            epoch: session.epoch,
45        }
46    }
47
48    fn retained_bytes_estimate(&self) -> usize {
49        std::mem::size_of::<Self>().saturating_add(serialized_bytes(self))
50    }
51}
52
53/// Reusable session-open layout derived from a fixed role topology and local types.
54#[derive(Debug, Clone)]
55pub struct SessionOpenPlan {
56    pub(crate) roles: Vec<String>,
57    pub(crate) role_ids: BTreeMap<String, u16>,
58    pub(crate) initial_types: Vec<(String, LocalTypeR, LocalTypeR)>,
59    pub(crate) edge_blueprint: Vec<((u16, u16), String, String)>,
60    pub(crate) active_branch_roles: Vec<String>,
61}
62
63impl SessionOpenPlan {
64    fn collect_protocol_edges(
65        role: &str,
66        local_type: &LocalTypeR,
67        role_ids: &BTreeMap<String, u16>,
68        edges: &mut BTreeSet<(u16, u16)>,
69    ) {
70        match local_type {
71            LocalTypeR::End | LocalTypeR::Var(_) => {}
72            LocalTypeR::Mu { body, .. } => {
73                Self::collect_protocol_edges(role, body, role_ids, edges);
74            }
75            LocalTypeR::Send { partner, branches } => {
76                if let (Some(from_id), Some(to_id)) = (role_ids.get(role), role_ids.get(partner)) {
77                    if from_id != to_id {
78                        edges.insert((*from_id, *to_id));
79                    }
80                }
81                for (_, _, continuation) in branches {
82                    Self::collect_protocol_edges(role, continuation, role_ids, edges);
83                }
84            }
85            LocalTypeR::Recv { partner, branches } => {
86                if let (Some(from_id), Some(to_id)) = (role_ids.get(partner), role_ids.get(role)) {
87                    if from_id != to_id {
88                        edges.insert((*from_id, *to_id));
89                    }
90                }
91                for (_, _, continuation) in branches {
92                    Self::collect_protocol_edges(role, continuation, role_ids, edges);
93                }
94            }
95        }
96    }
97
98    /// Build a reusable open plan from a role list and initial local types.
99    ///
100    /// # Panics
101    ///
102    /// Panics if an internally assigned role id does not map back into the
103    /// canonical `roles` slice while constructing the edge blueprint.
104    #[must_use]
105    pub fn new(roles: &[String], initial_types: &BTreeMap<String, LocalTypeR>) -> Self {
106        let role_ids = SessionState::build_role_ids(roles);
107        let mut planned_types = Vec::with_capacity(roles.len());
108        let mut active_branch_roles = Vec::new();
109        for role in roles {
110            if let Some(original) = initial_types.get(role) {
111                let current = unfold_mu(original);
112                if SessionState::branch_shape(&current).is_some() {
113                    active_branch_roles.push(role.clone());
114                }
115                planned_types.push((role.clone(), current, original.clone()));
116            }
117        }
118
119        let mut protocol_edges = BTreeSet::new();
120        for role in roles {
121            if let Some(original) = initial_types.get(role) {
122                Self::collect_protocol_edges(role, original, &role_ids, &mut protocol_edges);
123            }
124        }
125        let mut edge_blueprint = Vec::with_capacity(protocol_edges.len());
126        for (from_id, to_id) in protocol_edges {
127            let from = roles
128                .get(usize::from(from_id))
129                .expect("sender role id must index the session-open role set")
130                .clone();
131            let to = roles
132                .get(usize::from(to_id))
133                .expect("receiver role id must index the session-open role set")
134                .clone();
135            edge_blueprint.push(((from_id, to_id), from, to));
136        }
137
138        Self {
139            roles: roles.to_vec(),
140            role_ids,
141            initial_types: planned_types,
142            edge_blueprint,
143            active_branch_roles,
144        }
145    }
146
147    /// Canonical role ordering for this plan.
148    #[must_use]
149    pub fn roles(&self) -> &[String] {
150        &self.roles
151    }
152
153    /// Directed protocol edges needed by this session.
154    #[must_use]
155    pub fn edge_blueprint(&self) -> &[((u16, u16), String, String)] {
156        &self.edge_blueprint
157    }
158}
159
160/// Approximate retained state for the session store.
161#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
162pub struct SessionStoreMemoryUsage {
163    /// Number of live sessions still resident in the store.
164    pub live_sessions: usize,
165    /// Number of closed/cancelled/faulted sessions still resident in the store.
166    pub live_closed_sessions: usize,
167    /// Number of archived closed-session summaries retained after reaping.
168    pub archived_closed_sessions: usize,
169    /// Number of live endpoint type entries.
170    pub live_local_type_entries: usize,
171    /// Number of live directed buffers.
172    pub live_buffer_count: usize,
173    /// Number of live buffered messages.
174    pub live_buffered_messages: usize,
175    /// Number of live edge-bound handlers.
176    pub live_edge_handler_count: usize,
177    /// Number of live auth leaves across sessions.
178    pub live_auth_leaf_count: usize,
179    /// Number of live auth trees.
180    pub live_auth_tree_count: usize,
181    /// Number of live auth roots.
182    pub live_auth_root_count: usize,
183    /// Estimated retained bytes by session-store subsystem.
184    pub retained_bytes: SessionStoreRetainedBytes,
185}
186
187/// Estimated retained bytes for session-store subsystems.
188#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
189pub struct SessionStoreRetainedBytes {
190    /// Live session metadata excluding dedicated subsystems below.
191    pub live_sessions: usize,
192    /// Archived closed-session summaries.
193    pub archived_closed: usize,
194    /// Local type storage and endpoint bindings.
195    pub local_types: usize,
196    /// Buffer storage and buffered payloads.
197    pub buffers: usize,
198    /// Edge-trace storage.
199    pub traces: usize,
200    /// Auth leaves, trees, and roots.
201    pub auth: usize,
202    /// Handler bindings and defaults.
203    pub handlers: usize,
204    /// Aggregate retained bytes across all session-store subsystems.
205    pub total: usize,
206}
207
208/// Session identifier. Each session gets a unique ID within the ProtocolMachine.
209pub type SessionId = usize;
210
211/// Stable host/runtime owner identifier for one session capability.
212pub type FragmentOwnerId = String;
213
214/// Ownership generation/epoch used to reject stale capabilities.
215pub type OwnershipEpoch = u64;
216
217/// Identifier for one staged ownership operation.
218pub type OwnershipClaimId = u64;
219
220/// Identifier for one issued authority witness.
221pub type AuthorityWitnessId = u64;
222
223/// Handler identifier for edge-bound runtime dispatch.
224pub type HandlerId = String;
225type HandlerNumericId = u16;
226type LabelNumericId = u16;
227type EdgeKey = (u16, u16);
228type LocalBranches<'a> = &'a [(Label, Option<ValType>, LocalTypeR)];
229type HandlerIndexBuild = (
230    BTreeMap<HandlerId, HandlerNumericId>,
231    Vec<HandlerId>,
232    BTreeMap<EdgeKey, HandlerNumericId>,
233    Option<HandlerNumericId>,
234);
235
236#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
237pub(crate) enum BranchDirection {
238    Send,
239    Recv,
240}
241
242#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
243pub(crate) struct CachedBranch {
244    pub(crate) direction: BranchDirection,
245    pub(crate) partner: String,
246    pub(crate) expected_type: Option<ValType>,
247    pub(crate) continuation: LocalTypeR,
248}
249
250/// Built-in fallback handler id used when no edge-specific binding exists.
251pub(crate) const DEFAULT_HANDLER_ID: &str = "default_handler";
252
253fn default_handler_id() -> HandlerId {
254    DEFAULT_HANDLER_ID.to_string()
255}
256
257fn serialized_bytes<T: Serialize>(value: &T) -> usize {
258    crate::serialization::binary_size(value)
259}
260
261/// Edge between two roles in a session (directed: sender → receiver).
262#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
263pub struct Edge {
264    /// Session scope for this edge.
265    pub sid: SessionId,
266    /// Sender role name.
267    pub sender: String,
268    /// Receiver role name.
269    pub receiver: String,
270}
271
272impl Edge {
273    /// Construct a sid-qualified edge.
274    #[must_use]
275    pub fn new(sid: SessionId, sender: impl Into<String>, receiver: impl Into<String>) -> Self {
276        Self {
277            sid,
278            sender: sender.into(),
279            receiver: receiver.into(),
280        }
281    }
282}
283
284#[derive(Debug, Deserialize)]
285struct EdgeJson {
286    sid: Option<SessionId>,
287    sender: String,
288    receiver: String,
289}
290
291/// Decode an edge from JSON.
292///
293/// # Errors
294///
295/// Returns an error when fields are missing.
296pub fn decode_edge_json(
297    value: &JsonValue,
298    session_hint: Option<SessionId>,
299) -> Result<Edge, String> {
300    let raw: EdgeJson =
301        serde_json::from_value(value.clone()).map_err(|e| format!("invalid edge json: {e}"))?;
302
303    let sid = raw
304        .sid
305        .or(session_hint)
306        .ok_or_else(|| "missing sid in edge json".to_string())?;
307    Ok(Edge::new(sid, raw.sender, raw.receiver))
308}
309
310/// Session status.
311#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
312pub enum SessionStatus {
313    /// Session is active and processing messages.
314    Active,
315    /// Session is draining buffered messages before close.
316    Draining,
317    /// Session is closed normally.
318    Closed,
319    /// Session was cancelled.
320    Cancelled,
321    /// Session faulted.
322    Faulted {
323        /// Reason for the fault.
324        reason: String,
325    },
326}
327
328/// Current authority carried by a live ownership capability.
329#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
330pub enum OwnershipScope {
331    /// Full-session authority.
332    Session,
333    /// Fragment/boundary-scoped authority.
334    Fragments(BTreeSet<String>),
335}
336
337impl OwnershipScope {
338    /// Whether this scope authorizes full-session host mutation.
339    #[must_use]
340    pub fn allows_session_mutation(&self) -> bool {
341        matches!(self, Self::Session)
342    }
343}
344
345/// Capability proving the caller is the current owner for one session.
346#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
347pub struct OwnershipCapability {
348    /// Session covered by this capability.
349    pub session_id: SessionId,
350    /// Stable owner label.
351    pub owner_id: FragmentOwnerId,
352    /// Current ownership generation.
353    pub generation: OwnershipEpoch,
354    /// Authorized scope for this capability.
355    pub scope: OwnershipScope,
356}
357
358/// Receipt for an in-progress ownership transfer.
359#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
360pub struct OwnershipReceipt {
361    /// Session covered by the transfer.
362    pub session_id: SessionId,
363    /// Unique staged-claim identifier.
364    pub claim_id: OwnershipClaimId,
365    /// Previous owner label.
366    pub from_owner_id: FragmentOwnerId,
367    /// Previous owner generation.
368    pub from_generation: OwnershipEpoch,
369    /// Target owner label.
370    pub to_owner_id: FragmentOwnerId,
371    /// Generation that will become current on commit.
372    pub to_generation: OwnershipEpoch,
373    /// Scope granted if the transfer commits.
374    pub scope: OwnershipScope,
375}
376
377/// Witness proving a protocol-critical readiness check succeeded under the
378/// current owner capability.
379#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
380pub struct ReadinessWitness {
381    /// Unique witness identifier within one session.
382    pub witness_id: AuthorityWitnessId,
383    /// Session whose readiness was proven.
384    pub session_id: SessionId,
385    /// Owner label that requested the witness.
386    pub owner_id: FragmentOwnerId,
387    /// Owner generation that must still be live when the witness is consumed.
388    pub generation: OwnershipEpoch,
389    /// Scope under which the witness was issued.
390    pub scope: OwnershipScope,
391    /// Predicate/check reference justified by this witness.
392    pub predicate_ref: String,
393}
394
395/// Witness proving a session transitioned to an explicit cancellation path.
396#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
397pub struct CancellationWitness {
398    /// Unique witness identifier within one session.
399    pub witness_id: AuthorityWitnessId,
400    /// Session that was cancelled or faulted due to ownership failure.
401    pub session_id: SessionId,
402    /// Owner whose capability/lifecycle triggered the terminal transition.
403    pub owner_id: FragmentOwnerId,
404    /// Owner generation at the time the witness was issued.
405    pub generation: OwnershipEpoch,
406    /// Terminal ownership reason captured by the witness.
407    pub reason: OwnershipTerminalReason,
408}
409
410/// Witness proving a topology timeout was issued for one site.
411#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
412pub struct TimeoutWitness {
413    /// Unique witness identifier within one runtime.
414    pub witness_id: AuthorityWitnessId,
415    /// Site that timed out.
416    pub site: String,
417    /// Tick at which the timeout witness was issued.
418    pub issued_at_tick: u64,
419    /// Tick until which the timeout remains active.
420    pub until_tick: u64,
421}
422
423/// Typed authority artifact emitted or consumed by the runtime.
424#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
425pub enum AuthorityArtifact {
426    /// Live ownership capability issued or invalidated by the session store.
427    OwnershipCapability(OwnershipCapability),
428    /// Explicit ownership-transfer receipt issued/committed/rolled back.
429    OwnershipReceipt(OwnershipReceipt),
430    /// Readiness witness issued or consumed by an owner-gated flow.
431    Readiness(ReadinessWitness),
432    /// Cancellation witness issued by ownership failure handling.
433    Cancellation(CancellationWitness),
434    /// Timeout witness issued from topology ingress.
435    Timeout(TimeoutWitness),
436}
437
438/// Lifecycle event for one authority artifact.
439#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
440pub enum AuthorityAuditEvent {
441    /// Artifact was issued.
442    Issued,
443    /// Artifact was consumed exactly once.
444    Consumed,
445    /// Artifact became invalid because later semantic state revoked it.
446    Invalidated,
447    /// Transition artifact committed and became canonical.
448    Committed,
449    /// Transition artifact rolled back and did not become canonical.
450    RolledBack,
451    /// Artifact was rejected.
452    Rejected,
453    /// Artifact aged out of its validity window.
454    Expired,
455}
456
457impl From<AuthorityAuditEvent> for crate::capabilities::ProtocolCriticalCapabilityLifecycleState {
458    fn from(event: AuthorityAuditEvent) -> Self {
459        match event {
460            AuthorityAuditEvent::Issued => Self::Issued,
461            AuthorityAuditEvent::Consumed => Self::Consumed,
462            AuthorityAuditEvent::Invalidated => Self::Invalidated,
463            AuthorityAuditEvent::Committed => Self::Committed,
464            AuthorityAuditEvent::RolledBack => Self::RolledBack,
465            AuthorityAuditEvent::Rejected => Self::Rejected,
466            AuthorityAuditEvent::Expired => Self::Expired,
467        }
468    }
469}
470
471/// Deterministic audit record for witness issuance or consumption.
472#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
473pub struct AuthorityAuditRecord {
474    /// Optional runtime tick when the record was emitted.
475    pub tick: Option<u64>,
476    /// Artifact covered by this audit record.
477    pub artifact: AuthorityArtifact,
478    /// Event recorded for the artifact.
479    pub event: AuthorityAuditEvent,
480    /// Optional rejection or diagnostic reason.
481    pub reason: Option<String>,
482}
483
484/// Terminal reason recorded when ownership fails closed.
485#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
486pub enum OwnershipTerminalReason {
487    /// Current owner died or was abandoned by the host.
488    OwnerDied {
489        /// Owner that died.
490        owner_id: FragmentOwnerId,
491    },
492    /// Transfer was abandoned before commit.
493    TransferAbandoned {
494        /// Owner that abandoned the staged transfer.
495        owner_id: FragmentOwnerId,
496        /// Claim/receipt identifier for the abandoned transfer.
497        claim_id: OwnershipClaimId,
498    },
499    /// Transfer commit failed after staging.
500    TransferCommitFailed {
501        /// Owner whose staged transfer failed.
502        owner_id: FragmentOwnerId,
503        /// Claim/receipt identifier for the failed transfer.
504        claim_id: OwnershipClaimId,
505        /// Human-readable commit failure reason.
506        reason: String,
507    },
508}
509
510/// Errors surfaced by the runtime ownership contract.
511#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
512pub enum OwnershipError {
513    /// Session was not found.
514    SessionNotFound {
515        /// Session that was not found.
516        session_id: SessionId,
517    },
518    /// Session already has a current owner.
519    AlreadyClaimed {
520        /// Session that was already claimed.
521        session_id: SessionId,
522        /// Owner that already holds the claim.
523        current_owner_id: FragmentOwnerId,
524    },
525    /// Session does not currently have an owner.
526    Unclaimed {
527        /// Session that does not currently have an owner.
528        session_id: SessionId,
529    },
530    /// Capability generation or owner no longer matches live state.
531    StaleCapability {
532        /// Session whose live ownership state rejected the capability.
533        session_id: SessionId,
534        /// Owner label carried by the stale capability.
535        owner_id: FragmentOwnerId,
536        /// Generation expected by the caller.
537        expected_generation: OwnershipEpoch,
538        /// Generation currently live in the session store.
539        actual_generation: OwnershipEpoch,
540    },
541    /// Capability scope is too weak for the attempted operation.
542    ScopeViolation {
543        /// Session whose scope check failed.
544        session_id: SessionId,
545        /// Owner label that attempted the operation.
546        owner_id: FragmentOwnerId,
547        /// Minimum scope required for the operation.
548        required: OwnershipScope,
549        /// Actual live scope carried by the capability.
550        actual: OwnershipScope,
551    },
552    /// Another staged ownership transfer already exists.
553    TransferPending {
554        /// Session with an existing staged transfer.
555        session_id: SessionId,
556        /// Identifier of the staged transfer.
557        claim_id: OwnershipClaimId,
558    },
559    /// No staged ownership transfer exists.
560    TransferNotPending {
561        /// Session with no staged transfer.
562        session_id: SessionId,
563    },
564    /// Transfer receipt does not match live staged state.
565    ReceiptMismatch {
566        /// Session whose staged transfer did not match the receipt.
567        session_id: SessionId,
568        /// Identifier carried by the mismatched receipt.
569        claim_id: OwnershipClaimId,
570    },
571    /// Witness does not match current live authority state.
572    InvalidWitness {
573        /// Session whose witness validation failed.
574        session_id: SessionId,
575        /// Witness that failed validation.
576        witness_id: AuthorityWitnessId,
577        /// Human-readable mismatch reason.
578        reason: String,
579    },
580    /// Witness was already consumed.
581    WitnessConsumed {
582        /// Session whose witness was already consumed.
583        session_id: SessionId,
584        /// Witness id that cannot be reused.
585        witness_id: AuthorityWitnessId,
586    },
587    /// Ownership already terminated for this session.
588    Terminal {
589        /// Session whose ownership contract is terminal.
590        session_id: SessionId,
591        /// Recorded terminal ownership reason.
592        reason: OwnershipTerminalReason,
593    },
594}
595
596/// Host-routed session-local mutation guarded by ownership.
597#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
598pub enum SessionHostMutation {
599    /// Update the session default handler.
600    SetDefaultHandler {
601        /// New default handler binding.
602        handler: HandlerId,
603    },
604    /// Update one edge-bound handler.
605    UpdateEdgeHandler {
606        /// Edge whose handler binding should change.
607        edge: Edge,
608        /// New handler binding for the edge.
609        handler: HandlerId,
610    },
611    /// Update one edge coherence trace.
612    UpdateTrace {
613        /// Edge whose coherence trace should change.
614        edge: Edge,
615        /// New trace payload.
616        trace: Vec<ValType>,
617    },
618}
619
620#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
621pub(crate) struct PendingOwnershipTransfer {
622    pub(crate) receipt: OwnershipReceipt,
623}
624
625#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
626pub(crate) struct SessionOwnershipState {
627    pub(crate) current: Option<OwnershipCapability>,
628    pub(crate) pending_transfer: Option<PendingOwnershipTransfer>,
629    pub(crate) terminal_reason: Option<OwnershipTerminalReason>,
630    pub(crate) next_claim_id: OwnershipClaimId,
631    pub(crate) next_witness_id: AuthorityWitnessId,
632    pub(crate) issued_readiness: BTreeMap<AuthorityWitnessId, ReadinessWitness>,
633    pub(crate) consumed_witnesses: BTreeSet<AuthorityWitnessId>,
634    pub(crate) audit_log: Vec<AuthorityAuditRecord>,
635}
636
637impl Default for SessionOwnershipState {
638    fn default() -> Self {
639        Self {
640            current: None,
641            pending_transfer: None,
642            terminal_reason: None,
643            next_claim_id: 1,
644            next_witness_id: 1,
645            issued_readiness: BTreeMap::new(),
646            consumed_witnesses: BTreeSet::new(),
647            audit_log: Vec::new(),
648        }
649    }
650}
651
652/// Per-endpoint type tracking: current state + original for unfolding.
653#[derive(Debug, Clone, Serialize, Deserialize)]
654pub struct TypeEntry {
655    /// Current local type (advances with each completed instruction).
656    pub current: LocalTypeR,
657    /// Original local type (for unfolding recursive variables).
658    pub original: LocalTypeR,
659}
telltale_machine/session/overview.rs

telltale_machine/session/
overview.rs
